Merge pull request #4359 from unisonweb/travis/delay-kind-defaulting

This commit is contained in:
Arya Irani 2023-11-01 05:53:38 -07:00 committed by GitHub
commit ddf15e39b3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 34 additions and 3 deletions

View File

@ -28,7 +28,7 @@ import Data.Map.Strict qualified as Map
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
import Unison.DataDeclaration
import Unison.KindInference.Generate (declComponentConstraints, termConstraints)
import Unison.KindInference.Solve (KindError, verify, initialState, step)
import Unison.KindInference.Solve (KindError, verify, initialState, step, defaultUnconstrainedVars)
import Unison.KindInference.Solve.Monad (Env (..), SolveState, run, runGen)
import Unison.Prelude
import Unison.PrettyPrintEnv qualified as PrettyPrintEnv
@ -76,7 +76,7 @@ inferDecls ppe declMap =
handleComponents = verify <=< foldlM phi (initialState env)
where
phi b a = handleComponent b a
in handleComponents components
in defaultUnconstrainedVars <$> handleComponents components
-- | Break the decls into strongly connected components in reverse
-- topological order

View File

@ -2,6 +2,7 @@ module Unison.KindInference.Solve
( step,
verify,
initialState,
defaultUnconstrainedVars,
KindError (..),
ConstraintConflict (..),
)
@ -76,7 +77,7 @@ step e st cs =
in case unSolve action e st of
(res, finalState) -> case res of
Left e -> Left e
Right () -> Right (defaultUnconstrainedVars finalState)
Right () -> Right finalState
-- | Default any unconstrained vars to *
defaultUnconstrainedVars :: Var v => SolveState v loc -> SolveState v loc

View File

@ -54,6 +54,15 @@ unique type T a = T a
unique type S = S (T Nat)
```
Delay kind defaulting until all components are processed. Here `S`
constrains the kind of `T`'s `a` parameter, although `S` is not in
the same component as `T`.
```unison
unique type T a = T
unique type S = S (T Optional)
```
Catch invalid instantiation of `T`'s `a` parameter in `S`
```unison:error
unique type T a = T a

View File

@ -108,6 +108,27 @@ unique type T a = T a
unique type S = S (T Nat)
```
```ucm
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
unique type S
unique type T a
```
Delay kind defaulting until all components are processed. Here `S`
constrains the kind of `T`'s `a` parameter, although `S` is not in
the same component as `T`.
```unison
unique type T a = T
unique type S = S (T Optional)
```
```ucm
I found and typechecked these definitions in scratch.u. If you