Modify kind inference constraint generation order

add all decl constraints in component before any constructor constraints
This commit is contained in:
Travis Staton 2023-11-17 16:36:27 -05:00
parent 5571274311
commit 545fb19261
No known key found for this signature in database
GPG Key ID: 431DD911A00DAE49
3 changed files with 7 additions and 23 deletions

View File

@ -241,7 +241,7 @@ declComponentConstraintTree decls = do
-- Add a kind variable for every datatype
declKind <- pushType (Type.ref (DD.annotation $ asDataDecl decl) ref)
pure (ref, decl, declKind)
cts <- for decls \(ref, decl, declKind) -> do
(declConstraints, constructorConstraints) <- unzip <$> for decls \(ref, decl, declKind) -> do
let declAnn = DD.annotation $ asDataDecl decl
let declType = Type.ref declAnn ref
-- Unify the datatype with @k_1 -> ... -> k_n -> *@ where @n@ is
@ -275,8 +275,8 @@ declComponentConstraintTree decls = do
let finalDeclConstraints = case decl of
Left _effectDecl -> Constraint (IsAbility fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
Right _dataDecl -> Constraint (IsType fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
pure (StrictOrder finalDeclConstraints constructorConstraints)
pure (Node cts)
pure (finalDeclConstraints, constructorConstraints)
pure (Node declConstraints `StrictOrder` Node constructorConstraints)
-- | This is a helper to unify the kind constraints on type variables
-- across a decl's constructors.

View File

@ -1,4 +1,4 @@
```unison
```unison:error
structural type Foo f
= Foo (f ())
unique type Baz = Baz (Foo Bar)

View File

@ -10,25 +10,9 @@ unique type Bar
```ucm
Kind mismatch arising from
5 | unique type Bar
6 | = Bar Baz
3 | unique type Baz = Baz (Foo Bar)
Expected kind: Type
Given kind: Type -> Type
Foo expects an argument of kind: Type -> Type; however, it
is applied to Bar which has kind: Type.
```
🛑
The transcript failed due to an error in the stanza above. The error is:
Kind mismatch arising from
5 | unique type Bar
6 | = Bar Baz
Expected kind: Type
Given kind: Type -> Type