error extractors do cleanup of variable numbering

parser-typechecker/src/Unison/Type.hs

@@ -437,18 +437,35 @@ generalizeLowercase t = foldr (forall (ABT.annotation t)) t vars
   where vars = [ v | v <- Set.toList (ABT.freeVars t), isLow v]
         isLow v = all Char.isLower . take 1 . Text.unpack . Var.name $ v
 
--- | This function removes all variable shadowing from the type and reduces
--- fresh ids to the minimum possible to avoid ambiguity.
-cleanupVars1 :: Var v => AnnotatedType v a -> AnnotatedType v a
-cleanupVars1 t | not Settings.cleanupTypes = t
-cleanupVars1 t = let
-  varsByName = foldl' step Map.empty (ABT.allVars t)
+-- | This function removes all variable shadowing from the types and reduces
+-- fresh ids to the minimum possible to avoid ambiguity. Useful when showing
+-- two different types.
+cleanupVars :: Var v => [AnnotatedType v a] -> [AnnotatedType v a]
+cleanupVars ts | not Settings.cleanupTypes = ts
+cleanupVars ts = let
+  changedVars = cleanupVarsMap ts
+  in cleanupVars1' changedVars <$> ts
+
+-- Compute a variable replacement map from a collection of types, which
+-- can be passed to `cleanupVars1'`. This is used to cleanup variable ids
+-- for multiple related types, like when reporting a type error.
+cleanupVarsMap :: Var v => [AnnotatedType v a] -> Map.Map v v
+cleanupVarsMap ts = let
+  varsByName = foldl' step Map.empty (ts >>= ABT.allVars)
   step m v = Map.insertWith (++) (Var.name $ Var.reset v) [v] m
   changedVars = Map.fromList [ (v, Var.freshenId i v)
                              | (_, vs) <- Map.toList varsByName
                              , (v,i) <- nubOrd vs `zip` [0..]]
+  in changedVars
 
-  in ABT.changeVars changedVars t
+cleanupVars1' :: Var v => Map.Map v v -> AnnotatedType v a -> AnnotatedType v a
+cleanupVars1' = ABT.changeVars
+
+-- | This function removes all variable shadowing from the type and reduces
+-- fresh ids to the minimum possible to avoid ambiguity.
+cleanupVars1 :: Var v => AnnotatedType v a -> AnnotatedType v a
+cleanupVars1 t | not Settings.cleanupTypes = t
+cleanupVars1 t = let [t'] = cleanupVars [t] in t'
 
 -- This removes duplicates and normalizes the order of ability lists
 cleanupAbilityLists :: Var v => AnnotatedType v a -> AnnotatedType v a
@@ -462,6 +479,9 @@ cleanupAbilityLists t = ABT.visitPure go t where
          _ -> Just (effect (ABT.annotation t) es $ ABT.visitPure go v)
   go _ = Nothing
 
+cleanups :: Var v => [AnnotatedType v a] -> [AnnotatedType v a]
+cleanups ts = cleanupVars $ map cleanupAbilityLists ts
+
 cleanup :: Var v => AnnotatedType v a -> AnnotatedType v a
 cleanup t | not Settings.cleanupTypes = t
 cleanup t = cleanupVars1 . cleanupAbilityLists $ t

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

@@ -4,7 +4,8 @@
 module Unison.Typechecker.TypeError where
 
 import           Control.Applicative           (empty)
-import           Data.Foldable                 (asum)
+import           Data.Foldable                 (asum, toList)
+import           Data.Bifunctor                (second)
 import           Data.Functor                  (void)
 import           Data.Maybe                    (catMaybes)
 import           Prelude                       hiding (all, and, or)
@@ -195,7 +196,7 @@ booleanMismatch0 b ex = do
     (foundType, _, _) <- inSubtypes
     void $ Ex.some Ex.inCheck
     ex
-    pure foundType
+    pure $ Type.cleanup foundType
   pure (BooleanMismatch b mismatchLoc (sub foundType) n)
 
 existentialMismatch0
@@ -209,13 +210,13 @@ existentialMismatch0 em getExpectedLoc = do
   let sub t = C.apply ctx t
   mismatchSite <- Ex.innermostTerm
   let mismatchLoc = ABT.annotation mismatchSite
-  (foundType, expectedType, expectedLoc) <- Ex.unique $ do
+  ([foundType, expectedType], expectedLoc) <- Ex.unique $ do
     Ex.pathStart
     subtypes <- Ex.some Ex.inSubtype
     let (foundType, expectedType) = last subtypes
     void $ Ex.some Ex.inCheck
     expectedLoc <- getExpectedLoc
-    pure (foundType, expectedType, expectedLoc)
+    pure (Type.cleanups [foundType, expectedType], expectedLoc)
   pure $ ExistentialMismatch em (sub expectedType) expectedLoc
                                 (sub foundType) mismatchLoc
                                 -- todo : save type leaves too
@@ -227,7 +228,7 @@ ifBody = existentialMismatch0 IfBody (Ex.inSynthesizeApp >> Ex.inIfBody)
 vectorBody = existentialMismatch0 VectorBody (Ex.inSynthesizeApp >> Ex.inVector)
 matchBody = existentialMismatch0 CaseBody (Ex.inMatchBody >> Ex.inMatch)
 
-applyingNonFunction :: Ex.ErrorExtractor v loc (TypeError v loc)
+applyingNonFunction :: Var v => Ex.ErrorExtractor v loc (TypeError v loc)
 applyingNonFunction = do
   _ <- Ex.typeMismatch
   n <- Ex.errorNote
@@ -239,7 +240,7 @@ applyingNonFunction = do
         foundArgCount = length args
         -- unexpectedArgLoc = ABT.annotation arg
     whenM (expectedArgCount < foundArgCount) $ pure (f, arity0Type)
-  pure $ NotFunctionApplication f ft n
+  pure $ NotFunctionApplication f (Type.cleanup ft) n
 
 -- | Want to collect this info:
   -- The `n`th argument to `f` is `foundType`, but I was expecting `expectedType`.
@@ -252,7 +253,7 @@ applyingNonFunction = do
   --    `b` was chosen as `B`
   --    `c` was chosen as `C`
   -- (many colors / groups)
-applyingFunction :: forall v loc. Eq v => Ex.ErrorExtractor v loc (TypeError v loc)
+applyingFunction :: forall v loc. (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
 applyingFunction = do
   n <- Ex.errorNote
   ctx <- Ex.typeMismatch
@@ -266,7 +267,18 @@ applyingFunction = do
     let go :: v -> Maybe (v, C.Type v loc)
         go v = (v,) . Type.getPolytype <$> C.lookupSolved ctx v
         solvedVars = catMaybes (go <$> typeVars)
-    pure $ FunctionApplication f ft arg argIndex found expected leafs solvedVars n
+    let vm = Type.cleanupVarsMap $ [ft, found, expected]
+                                <> (fst <$> toList leafs)
+                                <> (snd <$> toList leafs)
+                                <> (snd <$> solvedVars)
+        cleanup = Type.cleanupVars1' vm . Type.cleanupAbilityLists
+    pure $ FunctionApplication f (cleanup ft)
+                                 arg argIndex
+                                 (cleanup found)
+                                 (cleanup expected)
+                                 ((\(a,b) -> (cleanup a, cleanup b)) <$> leafs)
+                                 (second cleanup <$> solvedVars)
+                                 n
 
 inSubtypes :: Ex.SubseqExtractor v loc (C.Type v loc,
                                         C.Type v loc,