From 545fb19261a6793165d2f52b345dbb08af790bb2 Mon Sep 17 00:00:00 2001 From: Travis Staton Date: Fri, 17 Nov 2023 16:36:27 -0500 Subject: [PATCH] Modify kind inference constraint generation order add all decl constraints in component before any constructor constraints --- .../src/Unison/KindInference/Generate.hs | 6 ++--- unison-src/transcripts/fix4397.md | 2 +- unison-src/transcripts/fix4397.output.md | 22 +++---------------- 3 files changed, 7 insertions(+), 23 deletions(-) diff --git a/parser-typechecker/src/Unison/KindInference/Generate.hs b/parser-typechecker/src/Unison/KindInference/Generate.hs index 31ec310e9..86267ef07 100644 --- a/parser-typechecker/src/Unison/KindInference/Generate.hs +++ b/parser-typechecker/src/Unison/KindInference/Generate.hs @@ -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. diff --git a/unison-src/transcripts/fix4397.md b/unison-src/transcripts/fix4397.md index 69db894e8..9f81185cc 100644 --- a/unison-src/transcripts/fix4397.md +++ b/unison-src/transcripts/fix4397.md @@ -1,4 +1,4 @@ -```unison +```unison:error structural type Foo f = Foo (f ()) unique type Baz = Baz (Foo Bar) diff --git a/unison-src/transcripts/fix4397.output.md b/unison-src/transcripts/fix4397.output.md index 01dba96e2..ea60d5943 100644 --- a/unison-src/transcripts/fix4397.output.md +++ b/unison-src/transcripts/fix4397.output.md @@ -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 -