Merge pull request #4366 from unisonweb/travis/kind-inference-context…

…-bug

Fix kind inference context bug

parser-typechecker/src/Unison/KindInference/Generate.hs

@@ -20,7 +20,7 @@ import Unison.KindInference.Constraint.Context (ConstraintContext (..))
 import Unison.KindInference.Constraint.Provenance (Provenance (..))
 import Unison.KindInference.Constraint.Provenance qualified as Provenance
 import Unison.KindInference.Constraint.Unsolved (Constraint (..))
-import Unison.KindInference.Generate.Monad (Gen, GeneratedConstraint, freshVar, insertType, lookupType, scopedType)
+import Unison.KindInference.Generate.Monad (Gen, GeneratedConstraint, freshVar, pushType, lookupType, scopedType)
 import Unison.KindInference.UVar (UVar)
 import Unison.Prelude
 import Unison.Reference (Reference)
@@ -239,7 +239,7 @@ declComponentConstraintTree ::
 declComponentConstraintTree decls = do
   decls <- for decls \(ref, decl) -> do
     -- Add a kind variable for every datatype
-    declKind <- insertType (Type.ref (DD.annotation $ asDataDecl decl) ref)
+    declKind <- pushType (Type.ref (DD.annotation $ asDataDecl decl) ref)
     pure (ref, decl, declKind)
   cts <- for decls \(ref, decl, declKind) -> do
     let declAnn = DD.annotation $ asDataDecl decl
@@ -413,7 +413,7 @@ builtinConstraintTree =
 
     constrain :: Kind -> (loc -> Type.Type v loc) -> Gen v loc (ConstraintTree v loc)
     constrain k t = do
-      kindVar <- insertType (t builtinAnnotation)
+      kindVar <- pushType (t builtinAnnotation)
       foldr Constraint (Node []) <$> constrainToKind (Provenance Builtin builtinAnnotation) kindVar k
 
 constrainToKind :: (Var v) => Provenance v loc -> UVar v loc -> Kind -> Gen v loc [GeneratedConstraint v loc]

parser-typechecker/src/Unison/KindInference/Generate/Monad.hs

@@ -4,20 +4,22 @@ module Unison.KindInference.Generate.Monad
     GeneratedConstraint,
     run,
     freshVar,
-    insertType,
-    deleteType,
+    pushType,
+    popType,
     scopedType,
     lookupType,
   )
 where
 
-import Data.Set qualified as Set
 import Control.Monad.State.Strict
 import Data.Functor.Compose
+import Data.List.NonEmpty (NonEmpty ((:|)))
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map.Strict qualified as Map
-import Unison.KindInference.Constraint.Unsolved (Constraint (..))
+import Data.Set qualified as Set
 import Unison.KindInference.Constraint.Provenance (Provenance)
-import Unison.KindInference.UVar (UVar(..))
+import Unison.KindInference.Constraint.Unsolved (Constraint (..))
+import Unison.KindInference.UVar (UVar (..))
 import Unison.Prelude
 import Unison.Symbol
 import Unison.Type qualified as T
@@ -27,7 +29,7 @@ type GeneratedConstraint v loc = Constraint (UVar v loc) v loc Provenance
 
 data GenState v loc = GenState
   { unifVars :: !(Set Symbol),
-    typeMap :: !(Map (T.Type v loc) (UVar v loc)),
+    typeMap :: !(Map (T.Type v loc) (NonEmpty (UVar v loc))),
     newVars :: [UVar v loc]
   }
   deriving stock (Generic)
@@ -36,52 +38,59 @@ newtype Gen v loc a = Gen
   { unGen :: GenState v loc -> (a, GenState v loc)
   }
   deriving
-    ( Functor
-    , Applicative
-    , Monad,
+    ( Functor,
+      Applicative,
+      Monad,
       MonadState (GenState v loc)
-    ) via State (GenState v loc)
-
+    )
+    via State (GenState v loc)
 
 run :: Gen v loc a -> GenState v loc -> (a, GenState v loc)
 run (Gen ma) st0 = ma st0
 
 -- | Create a unique @UVar@ associated with @typ@
 freshVar :: Var v => T.Type v loc -> Gen v loc (UVar v loc)
 freshVar typ = do
-  st@GenState{unifVars, newVars} <- get
+  st@GenState {unifVars, newVars} <- get
   let var :: Symbol
       var = freshIn unifVars (typed (Inference Other))
       uvar = UVar var typ
       unifVars' = Set.insert var unifVars
-  put st { unifVars = unifVars', newVars = uvar : newVars }
+  put st {unifVars = unifVars', newVars = uvar : newVars}
   pure uvar
 
--- | Lookup the @UVar@ associated with @t@, or create one if it
--- doesn't exist
-insertType :: Var v => T.Type v loc -> Gen v loc (UVar v loc)
-insertType t = do
+-- | Associate a fresh @UVar@ with @t@, push onto context
+pushType :: Var v => T.Type v loc -> Gen v loc (UVar v loc)
+pushType t = do
   GenState {typeMap} <- get
   (var, newTypeMap) <-
     let f = \case
-          Nothing -> Compose $ (\v -> (v, Just v)) <$> freshVar t
-          Just v -> Compose (pure (v, Just v))
+          Nothing -> Compose $ (\v -> (v, Just (v :| []))) <$> freshVar t
+          Just xs -> Compose $ (\v -> (v, Just (NonEmpty.cons v xs))) <$> freshVar t
      in getCompose $ Map.alterF f t typeMap
   modify \st -> st {typeMap = newTypeMap}
   pure var
 
 lookupType :: Var v => T.Type v loc -> Gen v loc (Maybe (UVar v loc))
 lookupType t = do
   GenState {typeMap} <- get
-  pure (Map.lookup t typeMap)
+  pure (NonEmpty.head <$> Map.lookup t typeMap)
 
-deleteType :: Var v => T.Type v loc -> Gen v loc ()
-deleteType t = do
-  modify \st -> st {typeMap = Map.delete t (typeMap st)}
+popType :: Var v => T.Type v loc -> Gen v loc ()
+popType t = do
+  modify \st -> st {typeMap = del (typeMap st)}
+  where
+    del m =
+      let f = \case
+            Nothing -> Nothing
+            Just (_ :| ys) -> case ys of
+              [] -> Nothing
+              x : xs -> Just (x :| xs)
+       in Map.alter f t m
 
 scopedType :: Var v => T.Type v loc -> (UVar v loc -> Gen v loc r) -> Gen v loc r
 scopedType t m = do
-  s <- insertType t
+  s <- pushType t
   r <- m s
-  deleteType t
+  popType t
   pure r

parser-typechecker/src/Unison/KindInference/Solve/Monad.hs

@@ -17,12 +17,13 @@ import Control.Lens (Lens', (%%~))
 import Control.Monad.Reader qualified as M
 import Control.Monad.State.Strict qualified as M
 import Data.Functor.Identity
+import Data.List.NonEmpty (NonEmpty)
 import Data.Map.Strict qualified as M
 import Data.Set qualified as Set
 import Unison.KindInference.Constraint.Solved (Constraint (..))
 import Unison.KindInference.Generate.Monad (Gen (..))
 import Unison.KindInference.Generate.Monad qualified as Gen
-import Unison.KindInference.UVar (UVar(..))
+import Unison.KindInference.UVar (UVar (..))
 import Unison.PatternMatchCoverage.UFMap qualified as U
 import Unison.Prelude
 import Unison.PrettyPrintEnv (PrettyPrintEnv)
@@ -38,7 +39,7 @@ data SolveState v loc = SolveState
   { unifVars :: !(Set Symbol),
     newUnifVars :: [UVar v loc],
     constraints :: !(U.UFMap (UVar v loc) (Descriptor v loc)),
-    typeMap :: !(Map (T.Type v loc) (UVar v loc))
+    typeMap :: !(Map (T.Type v loc) (NonEmpty (UVar v loc)))
   }
 
 data Descriptor v loc = Descriptor
@@ -81,7 +82,7 @@ runGen gena = do
   let ((cs, vs), st') = st & genStateL %%~ Gen.run gena'
   M.put st'
   traverse_ addUnconstrainedVar vs
-  M.modify \st -> st { newUnifVars = vs ++ newUnifVars st }
+  M.modify \st -> st {newUnifVars = vs ++ newUnifVars st}
   pure cs
 
 addUnconstrainedVar :: Var v => UVar v loc -> Solve v loc ()
@@ -110,4 +111,3 @@ find k = do
       M.put st {constraints = constraints'}
       pure descriptorConstraint
     Nothing -> error "find: Nothing"
-

unison-src/transcripts/bug-fix-4354.md

@@ -0,0 +1,13 @@
+```ucm:hide
+.> builtins.merge
+```
+
+```unison
+bonk : forall a. a -> a
+bonk x =
+  zonk : forall a. a -> a
+  zonk z = z
+  honk : a
+  honk = x
+  x
+```

unison-src/transcripts/bug-fix-4354.output.md

@@ -0,0 +1,21 @@
+```unison
+bonk : forall a. a -> a
+bonk x =
+  zonk : forall a. a -> a
+  zonk z = z
+  honk : a
+  honk = x
+  x
+```
+
+```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`:
+    
+      bonk : a -> a
+
+```