From 91294a21814487d8e9a7889669e4671f8349f31a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Thu, 9 Nov 2023 19:39:24 +0100 Subject: [PATCH] Add start on constructor type checking --- stdlib/cuda/wrapper.mc | 6 +-- stdlib/mexpr/ast-builder.mc | 12 +++-- stdlib/mexpr/ast.mc | 16 +++++-- stdlib/mexpr/boot-parser.mc | 3 +- stdlib/mexpr/cmp.mc | 9 +++- stdlib/mexpr/eq.mc | 8 +++- stdlib/mexpr/monomorphize.mc | 2 +- stdlib/mexpr/pprint.mc | 30 +++++++++--- stdlib/mexpr/type-check.mc | 86 +++++++++++++++++----------------- stdlib/mexpr/type-lift.mc | 12 ++--- stdlib/mexpr/type.mc | 11 +++-- stdlib/mexpr/unify.mc | 48 +++++++++++-------- stdlib/mexpr/utest-generate.mc | 4 +- stdlib/parser/tool.mc | 1 + stdlib/peval/include.mc | 2 +- 15 files changed, 150 insertions(+), 100 deletions(-) diff --git a/stdlib/cuda/wrapper.mc b/stdlib/cuda/wrapper.mc index f828b60f5..814c96dc7 100644 --- a/stdlib/cuda/wrapper.mc +++ b/stdlib/cuda/wrapper.mc @@ -91,7 +91,7 @@ lang CudaCWrapperBase = PMExprCWrapper + CudaAst + MExprAst + CudaCompile let fields = mapFromSeq cmpSID fieldsSeq in let ty = TyRecord {t with fields = fields} in optionMap - (lam id. TyCon {ident = id, info = t.info}) + (lam id. nitycon_ id t.info) (mapLookup ty cenv.revTypeEnv) else None () | ty & (TySeq {ty = elemTy} | TyTensor {ty = elemTy}) -> @@ -104,12 +104,12 @@ lang CudaCWrapperBase = PMExprCWrapper + CudaAst + MExprAst + CudaCompile else never in match env with CudaTargetEnv cenv in match mapLookup ty cenv.revTypeEnv with Some id then - Some (TyCon {ident = id, info = infoTy ty}) + Some (nitycon_ id (infoTy ty)) else None () | ty & (TyVariant _) -> match env with CudaTargetEnv cenv in match mapLookup ty cenv.revTypeEnv with Some id then - Some (TyCon {ident = id, info = infoTy ty}) + Some (nitycon_ id (infoTy ty)) else None () | TyAlias t -> lookupTypeIdent env t.content | ty -> Some ty diff --git a/stdlib/mexpr/ast-builder.mc b/stdlib/mexpr/ast-builder.mc index 7e1b59ddc..e8f23195d 100644 --- a/stdlib/mexpr/ast-builder.mc +++ b/stdlib/mexpr/ast-builder.mc @@ -92,9 +92,15 @@ let tyalias_ = use AliasTypeAst in lam display. lam content. TyAlias {display = display, content = content} -let ntycon_ = use ConTypeAst in - lam n. - TyCon {ident = n, info = NoInfo ()} +let nsitycon_ = use ConTypeAst in + lam n. lam d. lam i. + TyCon {ident = n, data = d, info = i} + +let nitycon_ = lam n. lam i. + nsitycon_ n tyunknown_ i + +let ntycon_ = lam n. + nitycon_ n (NoInfo ()) let tycon_ = lam s. ntycon_ (nameNoSym s) diff --git a/stdlib/mexpr/ast.mc b/stdlib/mexpr/ast.mc index 0f9730dea..9a5e91f78 100644 --- a/stdlib/mexpr/ast.mc +++ b/stdlib/mexpr/ast.mc @@ -5,6 +5,7 @@ include "name.mc" include "string.mc" include "stringid.mc" include "map.mc" +include "set.mc" ----------- -- TERMS -- @@ -1398,11 +1399,17 @@ end lang ConTypeAst = Ast syn Type = | TyCon {info : Info, - ident : Name} + ident : Name, + data : Type} sem tyWithInfo (info : Info) = | TyCon t -> TyCon {t with info = info} + sem smapAccumL_Type_Type (f : acc -> Type -> (acc, Type)) (acc : acc) = + | TyCon t -> + match f acc t.data with (acc, data) in + (acc, TyCon {t with data = data}) + sem infoTy = | TyCon r -> r.info end @@ -1424,13 +1431,14 @@ lang KindAst syn Kind = | Poly () | Mono () - | Row {fields : Map SID Type} + | Record {fields : Map SID Type} + | Data {types : Map Name (Set Name)} sem smapAccumL_Kind_Type : all acc. (acc -> Type -> (acc, Type)) -> acc -> Kind -> (acc, Kind) sem smapAccumL_Kind_Type (f : acc -> Type -> (acc, Type)) (acc : acc) = - | Row r -> + | Record r -> match mapMapAccum (lam acc. lam. lam e. f acc e) acc r.fields with (acc, flds) in - (acc, Row {r with fields = flds}) + (acc, Record {r with fields = flds}) | s -> (acc, s) diff --git a/stdlib/mexpr/boot-parser.mc b/stdlib/mexpr/boot-parser.mc index a87e8ad79..e67987aa2 100644 --- a/stdlib/mexpr/boot-parser.mc +++ b/stdlib/mexpr/boot-parser.mc @@ -274,7 +274,8 @@ lang BootParser = MExprAst + ConstTransformer else error "Parsing of non-empty variant types not yet supported" | 209 /-TyCon-/ -> TyCon {info = ginfo t 0, - ident = gname t 0} + ident = gname t 0, + data = TyUnknown { info = ginfo t 0 }} | 210 /-TyVar-/ -> TyVar {info = ginfo t 0, ident = gname t 0} diff --git a/stdlib/mexpr/cmp.mc b/stdlib/mexpr/cmp.mc index 9dbedd95d..c69d223d3 100644 --- a/stdlib/mexpr/cmp.mc +++ b/stdlib/mexpr/cmp.mc @@ -405,7 +405,10 @@ end lang ConTypeCmp = Cmp + ConTypeAst sem cmpTypeH = - | (TyCon t1, TyCon t2) -> nameCmp t1.ident t2.ident + | (TyCon t1, TyCon t2) -> + let nameDiff = nameCmp t1.ident t2.ident in + if eqi nameDiff 0 then cmpType t1.data t2.data + else nameDiff end lang VarTypeCmp = Cmp + VarTypeAst @@ -415,8 +418,10 @@ end lang KindCmp = Cmp + KindAst sem cmpKind = - | (Row l, Row r) -> + | (Record l, Record r) -> mapCmp cmpType l.fields r.fields + | (Data l, Data r) -> + mapCmp setCmp l.types r.types | (lhs, rhs) -> subi (constructorTag lhs) (constructorTag rhs) end diff --git a/stdlib/mexpr/eq.mc b/stdlib/mexpr/eq.mc index ed9dbeb06..5dd7b3709 100644 --- a/stdlib/mexpr/eq.mc +++ b/stdlib/mexpr/eq.mc @@ -632,7 +632,8 @@ lang ConTypeEq = Eq + ConTypeAst sem eqTypeH (typeEnv : EqTypeEnv) (free : EqTypeFreeEnv) (lhs : Type) = | rhs & TyCon r -> match unwrapType lhs with TyCon l then - if nameEq l.ident r.ident then Some free else None () + if nameEq l.ident r.ident then eqTypeH typeEnv free l.data r.data + else None () else None () end @@ -648,7 +649,7 @@ end lang KindEq = Eq + KindAst sem eqKind (typeEnv : EqTypeEnv) (free : EqTypeFreeEnv) = - | (Row l, Row r) -> + | (Record l, Record r) -> if eqi (mapSize l.fields) (mapSize r.fields) then mapFoldlOption (lam free. lam k1. lam v1. @@ -657,6 +658,9 @@ lang KindEq = Eq + KindAst else None ()) free l.fields else None () + | (Data l, Data r) -> + if mapEq setEq l.types r.types then Some free + else None () | (lhs, rhs) -> if eqi (constructorTag lhs) (constructorTag rhs) then Some free else None () diff --git a/stdlib/mexpr/monomorphize.mc b/stdlib/mexpr/monomorphize.mc index d19f61c3e..e5e65f837 100644 --- a/stdlib/mexpr/monomorphize.mc +++ b/stdlib/mexpr/monomorphize.mc @@ -764,7 +764,7 @@ lang MonomorphizeApply = MonomorphizeInstantiate + MonomorphizeResymbolize match mapLookup t.ident env.typeEnv with Some instEntry then let typeInst = findTypeInstantiation instEntry.polyType ty in match mapLookup typeInst instEntry.map with Some newId then - TyCon {ident = newId, info = infoTy ty} + TyCon {t with ident = newId, info = infoTy ty} else monoError [t.info] "Invalid type constructor instantiation" else diff --git a/stdlib/mexpr/pprint.mc b/stdlib/mexpr/pprint.mc index eef520a4f..2fd4b6ebb 100644 --- a/stdlib/mexpr/pprint.mc +++ b/stdlib/mexpr/pprint.mc @@ -1144,10 +1144,13 @@ lang VariantTypePrettyPrint = VariantTypeAst -- still use TyVariant in the AST and might get compilation errors for it. end -lang ConTypePrettyPrint = IdentifierPrettyPrint + ConTypeAst +lang ConTypePrettyPrint = IdentifierPrettyPrint + ConTypeAst + UnknownTypeAst sem getTypeStringCode (indent : Int) (env: PprintEnv) = | TyCon t -> - pprintTypeName env t.ident + match pprintTypeName env t.ident with (env, idstr) in + match t.data with TyUnknown {} then (env, idstr) else + match getTypeStringCode indent env t.data with (env, str) in + (env, join [str, ".", idstr]) end lang VarTypePrettyPrint = IdentifierPrettyPrint + VarTypeAst @@ -1157,12 +1160,21 @@ lang VarTypePrettyPrint = IdentifierPrettyPrint + VarTypeAst end lang KindPrettyPrint = PrettyPrint + RecordTypeAst + KindAst - sem getKindStringCode (indent : Int) (env : PprintEnv) (idstr : String) = - | Row r -> + sem getKindStringCode (indent : Int) (env : PprintEnv) = + | Record r -> let recty = TyRecord {info = NoInfo (), fields = r.fields} in match getTypeStringCode indent env recty with (env, recstr) in (env, join [init recstr, " ... ", [last recstr]]) - | _ -> (env, idstr) + | Data r -> + let tstr = + mapFoldWithKey (lam strs. lam t. lam ks. + snoc strs (join [ nameGetStr t, "{" + , strJoin ", " (map nameGetStr (setToSeq ks)) + , "}" ]) + ) "" r.types in + (env, join ["<", strJoin ", " tstr, ">"]) + | Poly () -> (env, "*") + | Mono () -> (env, "o") end lang AllTypePrettyPrint = IdentifierPrettyPrint + AllTypeAst + KindPrettyPrint @@ -1172,9 +1184,13 @@ lang AllTypePrettyPrint = IdentifierPrettyPrint + AllTypeAst + KindPrettyPrint sem getTypeStringCode (indent : Int) (env: PprintEnv) = | TyAll t -> match pprintVarName env t.ident with (env, idstr) in - match getKindStringCode indent env idstr t.kind with (env, varstr) in + match + match t.kind with Mono () | Poly () then (env, "") else + match getKindStringCode indent env t.kind with (env, kistr) in + (env, concat " :: " kistr) + with (env, kistr) in match getTypeStringCode indent env t.ty with (env, tystr) in - (env, join ["all ", varstr, ". ", tystr]) + (env, join ["all ", idstr, kistr, ". ", tystr]) end lang AppTypePrettyPrint = PrettyPrint + AppTypeAst diff --git a/stdlib/mexpr/type-check.mc b/stdlib/mexpr/type-check.mc index 36878ff2c..d8cf26470 100644 --- a/stdlib/mexpr/type-check.mc +++ b/stdlib/mexpr/type-check.mc @@ -155,16 +155,18 @@ lang VarTypeTCUnify = TCUnify + VarTypeAst else () end -lang MetaVarTypeTCUnify = TCUnify + MetaVarTypeUnify + UnifyRows + RecordTypeAst +lang MetaVarTypeTCUnify = TCUnify + MetaVarTypeUnify + UnifyRecords + RecordTypeAst sem addKinds : Unifier () -> UnifyEnv -> (Kind, Kind) -> Kind sem addKinds u env = - | (Row r1, Row r2) -> - match unifyRowsUnion u env r1.fields r2.fields with (_, fields) in - Row {r1 with fields = fields} - | (Row _ & rv, ! Row _ & tv) - | (! Row _ & tv, Row _ & rv) -> rv - | (Poly _, Poly _) -> Poly () - | (s1, s2) -> Mono () + | (Record r1, Record r2) -> + match unifyRecordsUnion u env r1.fields r2.fields with (_, fields) in + Record {r1 with fields = fields} + | (Data r1, Data r2) -> + Data {r1 with types = mapUnionWith setUnion r1.types r2.types} + | (Mono _ | Poly _, k & !(Mono _ | Poly _)) -> k + | (Poly _, k & (Poly _ | Mono _)) -> k + | (Mono _, Poly _ | Mono _) -> Mono () + | (k1, k2) -> u.err (Kinds (k1, k2)); error "impossible" sem unifyMeta u tcenv info env = | (TyMetaVar t1 & ty1, TyMetaVar t2 & ty2) -> @@ -181,9 +183,9 @@ lang MetaVarTypeTCUnify = TCUnify + MetaVarTypeUnify + UnifyRows + RecordTypeAst | (TyMetaVar t1 & ty1, !TyMetaVar _ & ty2) -> match deref t1.contents with Unbound tv in unifyCheck tcenv info tv ty2; - (match (tv.kind, ty2) with (Row r1, TyRecord r2) then - unifyRowsSubset u env r1.fields r2.fields - else match tv.kind with Row _ then u.err (Types (ty1, ty2)) else ()); + (match (tv.kind, ty2) with (Record r1, TyRecord r2) then + unifyRecordsSubset u env r1.fields r2.fields + else match tv.kind with Record _ then u.err (Types (ty1, ty2)) else ()); modref t1.contents (Link env.wrappedRhs) sem unifyCheckBase env info boundVars tv = @@ -333,7 +335,7 @@ lang MetaVarDisableGeneralize = MetaVarTypeAst sem disableRecordGeneralize (lvl : Level) = | TyMetaVar t & ty -> switch deref t.contents - case Unbound {kind = Row _} then + case Unbound {kind = Record _} then weakenMetaVars lvl ty case Unbound _ then () case Link tyL then @@ -385,9 +387,6 @@ lang ResolveType = ConTypeAst + AppTypeAst + AliasTypeAst + VariantTypeAst + else mkAppTy (resolveType info tycons constr) args - | TyUnknown _ & ty -> - ty - -- If we encounter a TyAlias, it means that the type was already processed by -- a previous call to typeCheck. | TyAlias t -> TyAlias t @@ -410,7 +409,7 @@ lang RemoveMetaVar = MetaVarTypeAst + UnknownTypeAst + RecordTypeAst sem removeMetaVarType = | TyMetaVar t -> switch deref t.contents - case Unbound {kind = Row x} then + case Unbound {kind = Record x} then TyRecord {info = t.info, fields = mapMap removeMetaVarType x.fields} case Unbound _ then TyUnknown { info = t.info } case Link ty then removeMetaVarType ty @@ -680,41 +679,42 @@ lang TypeTypeCheck = TypeCheck + TypeAst + VariantTypeAst + ResolveType end lang DataTypeCheck = TypeCheck + DataAst + FunTypeAst + ResolveType - -- NOTE(larshum, 2023-09-07): Verify that the annotated type of a constructor - -- is of the form we expect, and provide understandable error messages - -- otherwise. - sem _checkConstructorType : Info -> Name -> Type -> () - sem _checkConstructorType info ident = + sem _makeConstructorType : Info -> Name -> Type -> Type + sem _makeConstructorType info ident = | ty -> - recursive let isValidConstructorType = lam ty. - switch ty - case TyCon _ then true - case TyApp {lhs = lhs} then isValidConstructorType lhs - case _ then false + let msg = lam. join [ + "* Invalid type of constructor: ", nameGetStr ident, "\n", + "* The constructor should have a function type, where the\n", + "* right-hand side should refer to a constructor type.\n", + "* When type checking the expression\n" + ] in + recursive let substituteData = lam v. lam x. + switch x + case TyCon (t & {data = TyUnknown _}) then + TyCon { t with data = v } + case TyAlias t then + TyAlias { t with content = substituteData v t.content } + case _ then + smap_Type_Type (substituteData v) x end in match inspectType ty with TyArrow {to = to & (TyCon _ | TyApp _)} then - if isValidConstructorType to then () - else - let msg = join [ - "* Invalid type of constructor: ", nameGetStr ident, "\n", - "* The right-hand side should refer to a constructor type.\n", - "* When type checking the expression\n" - ] in - errorSingle [info] msg - else - let msg = join [ - "* Invalid type of constructor: ", nameGetStr ident, "\n", - "* The constructor should be given type A -> B, where B\n", - " is a fully applied datatype in scope.\n", - "* When type checking the expression\n" - ] in - errorSingle [info] msg + match getTypeArgs to with (TyCon t, _) then + let data = Data { + types = mapFromSeq nameCmp [ (t.ident, setOfSeq nameCmp [ ident ]) ] + } in + let x = nameSym "x" in + TyAll { info = info + , ident = x + , kind = data + , ty = substituteData (TyVar {info = info, ident = x}) ty } + else errorSingle [info] (msg ()) + else errorSingle [info] (msg ()) sem typeCheckExpr env = | TmConDef t -> let tyIdent = resolveType t.info env.tyConEnv t.tyIdent in - _checkConstructorType t.info t.ident tyIdent; + let tyIdent = _makeConstructorType t.info t.ident tyIdent in let inexpr = typeCheckExpr (_insertCon t.ident tyIdent env) t.inexpr in TmConDef {t with tyIdent = tyIdent, inexpr = inexpr, ty = tyTm inexpr} | TmConApp t -> diff --git a/stdlib/mexpr/type-lift.mc b/stdlib/mexpr/type-lift.mc index d7937ac47..799794a8a 100644 --- a/stdlib/mexpr/type-lift.mc +++ b/stdlib/mexpr/type-lift.mc @@ -87,11 +87,11 @@ lang TypeLiftAddRecordToEnv = TypeLiftBase + RecordTypeAst | TyRecord {fields = fields, info = info} & ty -> switch mapLookup fields env.records case Some name then - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in (env, tycon) case None _ then let name = nameSym "Rec" in - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in let env = {{env with records = mapInsert fields name env.records} with typeEnv = assocSeqInsert name ty env.typeEnv} @@ -106,11 +106,11 @@ lang TypeLiftAddSeqToEnv = TypeLiftBase + SeqTypeAst + ConTypeAst sem addSeqToEnv (env: TypeLiftEnv) = | TySeq {info = info, ty = innerTy} & ty -> match mapLookup innerTy env.seqs with Some name then - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in (env, tycon) else let name = nameSym "Seq" in - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in let env = {{env with seqs = mapInsert innerTy name env.seqs} with typeEnv = assocSeqInsert name ty env.typeEnv} in @@ -121,11 +121,11 @@ lang TypeLiftAddTensorToEnv = TypeLiftBase + TensorTypeAst + ConTypeAst sem addTensorToEnv (env : TypeLiftEnv) = | TyTensor {info = info, ty = innerTy} & ty -> match mapLookup innerTy env.tensors with Some name then - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in (env, tycon) else let name = nameSym "Tensor" in - let tycon = TyCon {ident = name, info = info} in + let tycon = nitycon_ name info in let env = {{env with tensors = mapInsert innerTy name env.tensors} with typeEnv = assocSeqInsert name ty env.typeEnv} in diff --git a/stdlib/mexpr/type.mc b/stdlib/mexpr/type.mc index 3205f996d..67d05a2e7 100644 --- a/stdlib/mexpr/type.mc +++ b/stdlib/mexpr/type.mc @@ -97,10 +97,11 @@ lang MetaVarTypePrettyPrint = IdentifierPrettyPrint + KindPrettyPrint + MetaVarT switch deref t.contents case Unbound t then match pprintVarName env t.ident with (env, idstr) in - match getKindStringCode indent env idstr t.kind with (env, str) in - let monoPrefix = - match t.kind with Mono _ then "_" else "" in - (env, concat monoPrefix str) + switch t.kind + case Poly () then (env, idstr) + case Mono () then (env, concat "_" idstr) + case _ then getKindStringCode indent env t.kind + end case Link ty then getTypeStringCode indent env ty end @@ -134,7 +135,7 @@ let newmonovar = use KindAst in let newpolyvar = use KindAst in newmetavar (Poly ()) let newrowvar = use KindAst in - lam fields. newmetavar (Row {fields = fields}) + lam fields. newmetavar (Record {fields = fields}) let newvar = newpolyvar diff --git a/stdlib/mexpr/unify.mc b/stdlib/mexpr/unify.mc index f819431a0..bb121c68d 100644 --- a/stdlib/mexpr/unify.mc +++ b/stdlib/mexpr/unify.mc @@ -23,7 +23,7 @@ lang Unify = Ast syn UnifyError = | Types (Type, Type) - | Rows (Map SID Type, Map SID Type) + | Records (Map SID Type, Map SID Type) | Kinds (Kind, Kind) type Unifier u = { @@ -55,10 +55,10 @@ lang Unify = Ast end -- Helper language providing functions to unify fields of record-like types -lang UnifyRows = Unify +lang UnifyRecords = Unify -- Check that 'm1' is a subset of 'm2' - sem unifyRowsSubset : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> u - sem unifyRowsSubset u env m1 = + sem unifyRecordsSubset : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> u + sem unifyRecordsSubset u env m1 = | m2 -> let f = lam acc. lam b. let unifier = @@ -66,24 +66,24 @@ lang UnifyRows = Unify match mapLookup k m2 with Some tyfield2 then unifyTypes u env (tyfield1, tyfield2) else - u.err (Rows (m1, m2)) + u.err (Records (m1, m2)) in u.combine acc unifier in foldl f u.empty (mapBindings m1) -- Check that 'm1' and 'm2' contain the same fields - sem unifyRowsStrict : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> u - sem unifyRowsStrict u env m1 = + sem unifyRecordsStrict : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> u + sem unifyRecordsStrict u env m1 = | m2 -> if eqi (mapSize m1) (mapSize m2) then - unifyRowsSubset u env m1 m2 + unifyRecordsSubset u env m1 m2 else - u.err (Rows (m1, m2)) + u.err (Records (m1, m2)) -- Check that the intersection of 'm1' and 'm2' unifies, then return their union - sem unifyRowsUnion : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> (u, Map SID Type) - sem unifyRowsUnion u env m1 = + sem unifyRecordsUnion : all u. Unifier u -> UnifyEnv -> Map SID Type -> Map SID Type -> (u, Map SID Type) + sem unifyRecordsUnion u env m1 = | m2 -> let f = lam acc. lam b. match b with (k, tyfield1) in @@ -126,14 +126,20 @@ lang AppTypeUnify = Unify + AppTypeAst (unifyTypes u env (t1.rhs, t2.rhs)) end -lang AllTypeUnify = UnifyRows + AllTypeAst +lang AllTypeUnify = UnifyRecords + AllTypeAst sem unifyBase u env = | (TyAll t1, TyAll t2) -> u.combine - (match (t1.kind, t2.kind) with (Row r1, Row r2) then - unifyRowsStrict u env r1.fields r2.fields - else if eqi (constructorTag t1.kind) (constructorTag t2.kind) then u.empty - else u.err (Kinds (t1.kind, t2.kind))) + (switch (t1.kind, t2.kind) + case (Record r1, Record r2) then + unifyRecordsStrict u env r1.fields r2.fields + case (Data r1, Data r2) then + if mapEq setEq r1.types r2.types then u.empty + else u.err (Kinds (t1.kind, t2.kind)) + case _ then + if eqi (constructorTag t1.kind) (constructorTag t2.kind) then u.empty + else u.err (Kinds (t1.kind, t2.kind)) + end) (let env = {env with boundNames = biInsert (t1.ident, t2.ident) env.boundNames} in unifyTypes u env (t1.ty, t2.ty)) end @@ -141,8 +147,10 @@ end lang ConTypeUnify = Unify + ConTypeAst sem unifyBase u env = | (TyCon t1 & ty1, TyCon t2 & ty2) -> - if nameEq t1.ident t2.ident then u.empty - else u.err (Types (ty1, ty2)) + if nameEq t1.ident t2.ident then + unifyTypes u env (t1.data, t2.data) + else + u.err (Types (ty1, ty2)) end lang BoolTypeUnify = Unify + BoolTypeAst @@ -177,10 +185,10 @@ lang TensorTypeUnify = Unify + TensorTypeAst unifyTypes u env (t1.ty, t2.ty) end -lang RecordTypeUnify = UnifyRows + RecordTypeAst +lang RecordTypeUnify = UnifyRecords + RecordTypeAst sem unifyBase u env = | (TyRecord t1, TyRecord t2) -> - unifyRowsStrict u env t1.fields t2.fields + unifyRecordsStrict u env t1.fields t2.fields end diff --git a/stdlib/mexpr/utest-generate.mc b/stdlib/mexpr/utest-generate.mc index a955511f8..843d7827e 100644 --- a/stdlib/mexpr/utest-generate.mc +++ b/stdlib/mexpr/utest-generate.mc @@ -81,9 +81,9 @@ let _stringTy = _seqTy _charTy let _tensorTy = lam ty. use MExprAst in TyTensor {ty = ty, info = _utestInfo} -let _conTy = lam id. +let _conTy = lam id. lam d. use MExprAst in - TyCon {ident = id, info = _utestInfo} + TyCon {ident = id, data = d, info = _utestInfo} let _varTy = lam id. use MExprAst in TyVar {ident = id, info = _utestInfo} diff --git a/stdlib/parser/tool.mc b/stdlib/parser/tool.mc index d3c7bb776..3238a21ad 100644 --- a/stdlib/parser/tool.mc +++ b/stdlib/parser/tool.mc @@ -201,6 +201,7 @@ let runParserGenerator : {synFile : String, outFile : String} -> () = lam args. result.ok (TyCon { ident = x.name.v , info = x.info + , data = tyunknown_ }) case VariableExpr x then result.ok (TyVar diff --git a/stdlib/peval/include.mc b/stdlib/peval/include.mc index 543f612a0..d9982b323 100644 --- a/stdlib/peval/include.mc +++ b/stdlib/peval/include.mc @@ -169,7 +169,7 @@ let includeTyConsNames = "FloatTypeAst_TyFloat","CharTypeAst_TyChar", "FunTypeAst_TyArrow", "SeqTypeAst_TySeq", "TensorTypeAst_TyTensor", "RecordTypeAst_TyRecord", "VariantTypeAst_TyVariant", "ConTypeAst_TyCon", "VarTypeAst_TyVar", - "KindAst_Poly", "KindAst_Mono", "KindAst_Row", + "KindAst_Poly", "KindAst_Mono", "KindAst_Record", "AllTypeAst_TyAll", "AppTypeAst_TyApp","AliasTypeAst_TyAlias"] let includeOtherFuncs =