Merge remote-tracking branch 'origin/trunk' into fix/845

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -38,12 +38,14 @@ where
 
 import Unison.Prelude
 
+import           Control.Lens                   (over, _2)
 import qualified Control.Monad.Fail            as MonadFail
 import           Control.Monad.Reader.Class
 import           Control.Monad.State            ( get
                                                 , put
                                                 , StateT
                                                 , runStateT
+                                                , evalState
                                                 )
 import           Data.Bifunctor                 ( first
                                                 , second
@@ -264,6 +266,49 @@ data InfoNote v loc
   | TopLevelComponent [(v, Type.Type v loc, RedundantTypeAnnotation)]
   deriving (Show)
 
+topLevelComponent :: Var v => [(v, Type.Type v loc, RedundantTypeAnnotation)] -> InfoNote v loc
+topLevelComponent = TopLevelComponent . fmap (over _2 removeSyntheticTypeVars)
+
+-- The typechecker generates synthetic type variables as part of type inference.
+-- This function converts these synthetic type variables to regular named type
+-- variables guaranteed to not collide with any other type variables.
+--
+-- It also attempts to pick "nice" type variable names, based on what sort of
+-- synthetic type variable it is and what type variable names are not already
+-- being used.
+removeSyntheticTypeVars :: Var v => Type.Type v loc -> Type.Type v loc
+removeSyntheticTypeVars typ =
+  flip evalState (Set.fromList (ABT.allVars typ), mempty) $ ABT.vmapM go typ
+  where
+  go v | Var.User _ <- Var.typeOf v = pure v -- user-provided type variables left alone
+       | otherwise                  = do
+         (used,curMappings) <- get
+         case Map.lookup v curMappings of
+           Nothing -> do
+             let v' = pickName used (Var.typeOf v)
+             put (Set.insert v' used, Map.insert v v' curMappings)
+             pure v'
+           Just v' -> pure v'
+  pickName used vt = ABT.freshIn used . Var.named $ case vt of
+    -- for each type of variable, we have some preferred variable
+    -- names that we like, if they aren't already being used
+    Var.Inference Var.Ability -> pick ["g","h","m","p"]
+    Var.Inference Var.Input -> pick ["a","b","c","i","j"]
+    Var.Inference Var.Output -> pick ["r","o"]
+    Var.Inference Var.Other -> pick ["t","u","w"]
+    Var.Inference Var.TypeConstructor -> pick ["f","k","d"]
+    Var.Inference Var.TypeConstructorArg -> pick ["v","w","y"]
+    Var.User n -> n
+    _ -> defaultName
+    where
+      used1CharVars = Set.fromList $ ABT.allVars typ >>= \v ->
+        case Text.unpack (Var.name . Var.reset $ v) of
+          [ch] -> [Text.singleton ch]
+          _ -> []
+      pick ns@(n:_) = fromMaybe n $ find (`Set.notMember` used1CharVars) ns
+      pick [] = error "impossible"
+      defaultName = "x"
+
 data Cause v loc
   = TypeMismatch (Context v loc)
   | IllFormedType (Context v loc)
@@ -799,14 +844,14 @@ noteTopLevelType e binding typ = case binding of
   Term.Ann' strippedBinding _ -> do
     inferred <- (Just <$> synthesize strippedBinding) `orElse` pure Nothing
     case inferred of
-      Nothing -> btw $ TopLevelComponent
+      Nothing -> btw $ topLevelComponent
         [(Var.reset (ABT.variable e), generalizeAndUnTypeVar typ, False)]
       Just inferred -> do
         redundant <- isRedundant typ inferred
-        btw $ TopLevelComponent
+        btw $ topLevelComponent
           [(Var.reset (ABT.variable e), generalizeAndUnTypeVar typ, redundant)]
   -- The signature didn't exist, so was definitely redundant
-  _ -> btw $ TopLevelComponent
+  _ -> btw $ topLevelComponent
     [(Var.reset (ABT.variable e), generalizeAndUnTypeVar typ, True)]
 
 -- | Synthesize the type of the given term, updating the context in the process.
@@ -1168,10 +1213,10 @@ annotateLetRecBindings isTop letrec =
     case withoutAnnotations of
       Just (_, vts') -> do
         r <- and <$> zipWithM isRedundant (fmap snd vts) (fmap snd vts')
-        btw $ TopLevelComponent ((\(v,b) -> (Var.reset v, b,r)) . unTypeVar <$> vts)
+        btw $ topLevelComponent ((\(v,b) -> (Var.reset v, b,r)) . unTypeVar <$> vts)
       -- ...(1) we'll assume all the user-provided annotations were needed
       Nothing -> btw
-        $ TopLevelComponent ((\(v, b) -> (Var.reset v, b, False)) . unTypeVar <$> vts)
+        $ topLevelComponent ((\(v, b) -> (Var.reset v, b, False)) . unTypeVar <$> vts)
     pure body
   -- If this isn't a top-level letrec, then we don't have to do anything special
   else fst <$> annotateLetRecBindings' True

unison-core/src/Unison/ABT.hs

@@ -140,6 +140,13 @@ vmap f (Term _ a out) = case out of
   Cycle r -> cycle' a (vmap f r)
   Abs v body -> abs' a (f v) (vmap f body)
 
+vmapM :: (Applicative m, Traversable f, Foldable f, Ord v2) => (v -> m v2) -> Term f v a -> m (Term f v2 a)
+vmapM f (Term _ a out) = case out of
+  Var v -> annotatedVar a <$> f v
+  Tm fa -> tm' a <$> traverse (vmapM f) fa
+  Cycle r -> cycle' a <$> vmapM f r
+  Abs v body -> abs' a <$> f v <*> vmapM f body
+
 amap :: (Functor f, Foldable f, Ord v) => (a -> a2) -> Term f v a -> Term f v a2
 amap = amap' . const
 

unison-src/transcripts/alias-many.output.md

@@ -350,11 +350,11 @@ I want to incorporate a few more from another namespace:
 .runar> find
 
   1.  List.adjacentPairs : [a] -> [(a, a)]
-  2.  List.all : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} Boolean
-  3.  List.any : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} Boolean
+  2.  List.all : (a ->{g} Boolean) ->{g} [a] ->{g} Boolean
+  3.  List.any : (a ->{g} Boolean) ->{g} [a] ->{g} Boolean
   4.  List.chunk : Nat -> [a] -> [[a]]
   5.  List.chunksOf : Nat -> [a] -> [[a]]
-  6.  List.dropWhile : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} [a]
+  6.  List.dropWhile : (a ->{g} Boolean) ->{g} [a] ->{g} [a]
   7.  List.first : [a] -> Optional a
   8.  List.init : [a] -> Optional [a]
   9.  List.intersperse : a -> [a] -> [a]
@@ -373,17 +373,17 @@ I want to incorporate a few more from another namespace:
   Added definitions:
   
     1.  List.adjacentPairs : [a] -> [(a, a)]
-    2.  List.all           : (a ->{𝕖} Boolean)
-                           ->{𝕖} [a]
-                           ->{𝕖} Boolean
-    3.  List.any           : (a ->{𝕖} Boolean)
-                           ->{𝕖} [a]
-                           ->{𝕖} Boolean
+    2.  List.all           : (a ->{g} Boolean)
+                           ->{g} [a]
+                           ->{g} Boolean
+    3.  List.any           : (a ->{g} Boolean)
+                           ->{g} [a]
+                           ->{g} Boolean
     4.  List.chunk         : Nat -> [a] -> [[a]]
     5.  List.chunksOf      : Nat -> [a] -> [[a]]
-    6.  List.dropWhile     : (a ->{𝕖} Boolean)
-                           ->{𝕖} [a]
-                           ->{𝕖} [a]
+    6.  List.dropWhile     : (a ->{g} Boolean)
+                           ->{g} [a]
+                           ->{g} [a]
     7.  List.first         : [a] -> Optional a
     8.  List.init          : [a] -> Optional [a]
     9.  List.intersperse   : a -> [a] -> [a]
@@ -412,11 +412,11 @@ I want to incorporate a few more from another namespace:
   10. builtin type Link.Term
   11. Link.Term : Term -> Link
   12. List.adjacentPairs : [a] -> [(a, a)]
-  13. List.all : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} Boolean
-  14. List.any : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} Boolean
+  13. List.all : (a ->{g} Boolean) ->{g} [a] ->{g} Boolean
+  14. List.any : (a ->{g} Boolean) ->{g} [a] ->{g} Boolean
   15. List.chunk : Nat -> [a] -> [[a]]
   16. List.chunksOf : Nat -> [a] -> [[a]]
-  17. List.dropWhile : (a ->{𝕖} Boolean) ->{𝕖} [a] ->{𝕖} [a]
+  17. List.dropWhile : (a ->{g} Boolean) ->{g} [a] ->{g} [a]
   18. List.first : [a] -> Optional a
   19. List.init : [a] -> Optional [a]
   20. List.intersperse : a -> [a] -> [a]

unison-src/transcripts/blocks.output.md

@@ -87,7 +87,7 @@ ex thing =
   
     ⍟ These new definitions are ok to `add`:
     
-      ex : (Nat ->{𝕖} Nat) ->{𝕖} Nat
+      ex : (Nat ->{g} Nat) ->{g} Nat
   
   Now evaluating any watch expressions (lines starting with
   `>`)... Ctrl+C cancels.
@@ -117,7 +117,7 @@ ex thing =
   
     ⍟ These new definitions are ok to `add`:
     
-      ex : (Nat ->{𝕖} Nat) ->{𝕖} Nat
+      ex : (Nat ->{g} Nat) ->{g} Nat
   
   Now evaluating any watch expressions (lines starting with
   `>`)... Ctrl+C cancels.
@@ -154,7 +154,7 @@ ex n =
   
     ⍟ These new definitions are ok to `add`:
     
-      ex    : n -> 𝕣
+      ex    : n -> r
       sumTo : Nat -> Nat
 
 ```
@@ -232,7 +232,7 @@ ex n =
   
     ⍟ These new definitions are ok to `add`:
     
-      ex : n -> 𝕣
+      ex : n -> r
 
 ```
 Just don't try to run it as it's an infinite loop!
@@ -309,7 +309,7 @@ ex n =
     ⍟ These new definitions are ok to `add`:
     
       ability SpaceAttack
-      ex : n ->{SpaceAttack} 𝕣
+      ex : n ->{SpaceAttack} r
 
 ```
 This is actually parsed as if you moved `zap` after the cycle it find itself a part of:
@@ -334,6 +334,6 @@ ex n =
     ⍟ These new definitions are ok to `add`:
     
       ability SpaceAttack
-      ex : n ->{SpaceAttack} 𝕣
+      ex : n ->{SpaceAttack} r
 
 ```

unison-src/transcripts/fix1063.output.md

@@ -14,8 +14,8 @@ noop = not . not
   
     ⍟ These new definitions are ok to `add`:
     
-      .    : ∀ o 𝕖 i1 i.
-               (i1 ->{𝕖} o) -> (i ->{𝕖} i1) -> i ->{𝕖} o
+      .    : ∀ o g i1 i.
+               (i1 ->{g} o) -> (i ->{g} i1) -> i ->{g} o
       noop : Boolean -> Boolean
 
 ```
@@ -24,7 +24,7 @@ noop = not . not
 
   ⍟ I've added these definitions:
   
-    .    : ∀ o 𝕖 i1 i. (i1 ->{𝕖} o) -> (i ->{𝕖} i1) -> i ->{𝕖} o
+    .    : ∀ o g i1 i. (i1 ->{g} o) -> (i ->{g} i1) -> i ->{g} o
     noop : Boolean -> Boolean
 
 .> view noop

unison-src/transcripts/fix1390.md

@@ -0,0 +1,28 @@
+
+```ucm
+.> builtins.merge
+```
+
+```unison
+-- List.map : (a -> b) -> [a] -> [b]
+List.map f =
+  go acc = cases
+    [] -> acc
+    h +: t -> go (acc :+ f h) t
+  go []
+```
+
+```ucm
+.> add
+.> view List.map
+```
+
+```unison
+List.map2 : (g -> g2) -> [g] -> [g2]
+List.map2 f =
+  unused = "just to give this a different hash"
+  go acc = cases
+    [] -> acc
+    h +: t -> go (acc :+ f h) t
+  go []
+```

unison-src/transcripts/fix1390.output.md

@@ -0,0 +1,65 @@
+
+```ucm
+.> builtins.merge
+
+  Done.
+
+```
+```unison
+-- List.map : (a -> b) -> [a] -> [b]
+List.map f =
+  go acc = cases
+    [] -> acc
+    h +: t -> go (acc :+ f h) t
+  go []
+```
+
+```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`:
+    
+      List.map : (i ->{g} o) ->{g} [i] ->{g} [o]
+
+```
+```ucm
+.> add
+
+  ⍟ I've added these definitions:
+  
+    List.map : (i ->{g} o) ->{g} [i] ->{g} [o]
+
+.> view List.map
+
+  List.map : (i ->{g} o) ->{g} [i] ->{g} [o]
+  List.map f =
+    go acc = cases
+      []     -> acc
+      h +: t -> go (acc :+ f h) t
+    go []
+
+```
+```unison
+List.map2 : (g -> g2) -> [g] -> [g2]
+List.map2 f =
+  unused = "just to give this a different hash"
+  go acc = cases
+    [] -> acc
+    h +: t -> go (acc :+ f h) t
+  go []
+```
+
+```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`:
+    
+      List.map2 : (g ->{h} g2) ->{h} [g] ->{h} [g2]
+
+```

unison-src/transcripts/lambdacase.output.md

@@ -16,7 +16,7 @@ isEmpty x = match x with
   
     ⍟ These new definitions are ok to `add`:
     
-      isEmpty : [𝕩] -> Boolean
+      isEmpty : [t] -> Boolean
 
 ```
 Here's the same function written using `cases` syntax:
@@ -35,7 +35,7 @@ isEmpty2 = cases
   
     ⍟ These new definitions are ok to `add`:
     
-      isEmpty2 : [𝕩] -> Boolean
+      isEmpty2 : [t] -> Boolean
         (also named isEmpty)
 
 ```
@@ -44,7 +44,7 @@ Notice that Unison detects this as an alias of `isEmpty`, and if we view `isEmpt
 ```ucm
 .> view isEmpty
 
-  isEmpty : [𝕩] -> Boolean
+  isEmpty : [t] -> Boolean
   isEmpty = cases
     [] -> true
     _  -> false
@@ -71,7 +71,7 @@ merge xs ys = match (xs, ys) with
 
   ⍟ I've added these definitions:
   
-    merge : [a] ->{𝕖} [a] ->{𝕖} [a]
+    merge : [a] ->{g} [a] ->{g} [a]
 
 ```
 Here's a version using `cases`:
@@ -94,7 +94,7 @@ merge2 = cases
   
     ⍟ These new definitions are ok to `add`:
     
-      merge2 : [a] ->{𝕖} [a] ->{𝕖} [a]
+      merge2 : [a] ->{g} [a] ->{g} [a]
         (also named merge)
 
 ```

unison-src/transcripts/squash.output.md

@@ -177,7 +177,7 @@ no more = no more
   ⍟ I've added these definitions:
   
     babyDon'tHurtMe : Text
-    no              : more -> 𝕣
+    no              : more -> r
     whatIsLove      : Text
 
 ```
@@ -294,7 +294,7 @@ Alice then squash merges into `trunk`, as does Bob. It's as if Alice and Bob bot
   Added definitions:
   
     1. babyDon'tHurtMe : Text
-    2. no              : more -> 𝕣
+    2. no              : more -> r
     3. whatIsLove      : Text
   
   Tip: You can use `todo` to see if this generated any work to
@@ -397,7 +397,7 @@ This time, we'll first squash Alice and Bob's changes together before squashing
   
     1. babyDon'tHurtMe   : Text
     2. bodaciousNumero   : Nat
-    3. no                : more -> 𝕣
+    3. no                : more -> r
     4. productionReadyId : x -> x
     5. superRadNumber    : Nat
     6. whatIsLove        : Text

unison-src/transcripts/todo-bug-builtins.output.md

@@ -65,7 +65,7 @@ complicatedMathStuff x = todo "Come back and to something with x here"
   
     ⍟ These new definitions are ok to `add`:
     
-      complicatedMathStuff : x -> 𝕣
+      complicatedMathStuff : x -> r
 
 ```
 ## Bug