🔥fix - Discard equality evidence with superclasses

src/Control/Monad/Infer.hs

@@ -630,9 +630,10 @@ instance Note TypeError Style where
                                          , f [annotation rs]
                                          , empty ])
                  in
-                  k (vsep [ indent 2 $ bullet "When checking that this expression has type"
-                          , indent 5 (Right <$> displayType t)
-                          , nest (-2) $ f [annotation ex] ])
+                  k (vsep [ indent 2 . bullet $ "When checking that this expression"
+                          , nest (-2) $ f [annotation ex]
+                          , indent 2 $ "has type" <+> nest 4 (Right <$> displayType t)
+                          ])
              BySubsumption s t ->
                vsep [ indent 2 $ bullet "When checking that the type"
                     , indent 5 (Right <$> displayType s)
@@ -671,7 +672,7 @@ instance Note TypeError Style where
                     , indent 2 $ bullet "Arising in the" <+> (Right <$> blameOf rs)
                     , nest (-2) $ f [annotation rs]
                     ]
-             ByConstraint p -> 
+             ByConstraint p ->
                vsep [ indent 2 $ "Where the type variable" <+> sk (pretty v)
                     , indent 2 "was made rigid because of a quantified constraint:"
                     , indent 2 (Right <$> displayType p)

src/Core/Lint.hs

@@ -372,6 +372,7 @@ checkCoercion s = checkCo where
   checkCo (CoercionVar x) =
     case VarMap.lookup (toVar x) (vars s) of
       Just (AppTy (AppTy _ l) r, _) -> pure (l, r)
+      Just _ -> pushError (InvalidCoercion (CoercionVar x))
       _ -> pure (VarTy (fromVar tyvarA), VarTy (fromVar tyvarB))
 
   checkCo (Nth co i) =

src/Types/Unify.hs

@@ -848,7 +848,11 @@ lookupEquality class_info scope assum a b = normal <|> fundepEquality where
   normal =
     let choices = filter ((/= Superclass) . view implSort) $
           find (TyApps tyEq [a, b]) scope <> find (TyApps tyEq [b, a]) scope
-     in assert (all ((== LocalAssum) . view implSort) choices) (map makeCo choices)
+
+        equality_invariants xs =
+             all ((== LocalAssum) . view implSort) xs
+          && none (not . null . view implPre) xs
+     in assert (equality_invariants choices) (map makeCo choices)
 
   makeCo ImplChoice{..} =
     case _implClass of
@@ -863,7 +867,7 @@ lookupEquality class_info scope assum a b = normal <|> fundepEquality where
           a :: Type Typed
           used x = map (implClass .~ x)
 
-  find_ffs t = map snd . filter (matches tau . view implHead . snd) . concatMap splat . Map.toList . keys where
+  find_ffs t = map snd . filter (null . view implPre . snd) . filter (matches tau . view implHead . snd) . concatMap splat . Map.toList . keys where
     tau = transformType go t
     splat (x, t) = map (x,) t
     go (TySkol v) | Just x <- assum ^. at (v ^. skolIdent) = x
@@ -1120,7 +1124,10 @@ skolemise motive wt@(TyPi (Implicit ity) t) = do
       go x = do
         var <- genName
         pure ([Capture var (internal, x)], insert internal LocalAssum var x (MagicInfo []) scp)
+
   (pat, scope) <- go ity
+  traceM (show (pretty ity))
+
   let wrap ex | an <- annotation ex =
         Fun (EvParam (PTuple pat (an, ity)))
           (ExprWrapper omega ex (an, ty)) (an, wt)

tests/types/class/quantified-eq-loopy.ml

@@ -0,0 +1,6 @@
+let unsafe_coerce : forall 'a 'b. 'a -> 'b =
+  let foo : forall 'a 'b. ('a ~ 'b => 'a ~ 'b) => 'a -> 'b =
+    fun x -> x
+  fun x -> foo x
+
+let foo : string = unsafe_coerce 10

tests/types/class/quantified-eq-loopy.out

@@ -0,0 +1,13 @@
+quantified-eq-loopy.ml[3:14 ..3:14]: error
+  Could not match the rigid type variable 'a with the type 'b
+
+  • Arising in this expression
+  │ 
+3 │     fun x -> x
+  │              ^
+
+  • When checking that this expression
+  │ 
+3 │     fun x -> x
+  │     ^^^^^^^^^^
+  has type forall 'a 'b. ('a ~ 'b => 'a ~ 'b) => 'a -> 'b

tests/types/fail_skolem_poly.out

@@ -6,11 +6,11 @@ fail_skolem_poly.ml[3:32 ..3:32]: error
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                                ^
 
-  • When checking that this expression has type
-     forall 'a. 'a -> 'a
+  • When checking that this expression
   │ 
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                       ^^^^^^^^^^^^^^
+  has type forall 'a. 'a -> 'a
 fail_skolem_poly.ml[3:32 ..3:36]: error
   Could not match the rigid type variable 'a with the type int
 
@@ -19,8 +19,8 @@ fail_skolem_poly.ml[3:32 ..3:36]: error
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                                ^^^^^
 
-  • When checking that this expression has type
-     forall 'a. 'a -> 'a
+  • When checking that this expression
   │ 
 3 │ let poly_fail = poly (fun x -> x + 1)
   │                       ^^^^^^^^^^^^^^
+  has type forall 'a. 'a -> 'a

tests/types/fail_skolem_pure.out

@@ -6,8 +6,8 @@ fail_skolem_pure.ml[2:32 ..2:32]: error
 2 │ let pure_fail = pure (fun x -> x)
   │                                ^
 
-  • When checking that this expression has type
-     forall 'a. 'a -> 'f 'a
+  • When checking that this expression
   │ 
 2 │ let pure_fail = pure (fun x -> x)
   │                       ^^^^^^^^^^
+  has type forall 'a. 'a -> 'f 'a

tests/types/gadt/fail_term.out

@@ -11,8 +11,8 @@ fail_term.ml[16:3 ..16:30]: error
 16 │   Lam (Lam (Var (There Here)))
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-  • When checking that this expression has type
-     forall 'a 'b. term unit ('a -> 'b -> 'b)
+  • When checking that this expression
    │ 
 16 │   Lam (Lam (Var (There Here)))
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  has type forall 'a 'b. term unit ('a -> 'b -> 'b)

tests/types/wildcards/wild05.out

@@ -6,8 +6,8 @@ wild05.ml[1:24 ..1:24]: error
 1 │ let f (x : 'a) : int = x
   │                        ^
 
-  • When checking that this expression has type
-     forall 'a. 'a -> int
+  • When checking that this expression
   │ 
 1 │ let f (x : 'a) : int = x
   │       ^^^^^^^^^^^^^^^^^^
+  has type forall 'a. 'a -> int