Unwrap casts before checking vars in eager unifier
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Thu, 5 Jul 2018 18:21:43 +0000 (14:21 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 10 Jul 2018 23:07:23 +0000 (19:07 -0400)
Previously, checking whether (tv |> co) ~ (tv |> co) got deferred,
because we looked for vars before stripping casts. (The left type
would get stripped, and then tv ~ (tv |> co) would scare the occurs-
checker.)

This opportunity for improvement presented itself in other work.
This is just an optimization. Some programs can now report more
errors simultaneously.

compiler/typecheck/TcUnify.hs
testsuite/tests/partial-sigs/should_fail/T12634.stderr
testsuite/tests/partial-sigs/should_fail/T14040a.stderr
testsuite/tests/partial-sigs/should_fail/T14584.stderr
testsuite/tests/polykinds/T12593.stderr
testsuite/tests/polykinds/T14846.stderr
testsuite/tests/typecheck/should_compile/T2494.stderr
testsuite/tests/typecheck/should_fail/VtaFail.stderr

index 08a5c59..410277c 100644 (file)
@@ -1304,6 +1304,17 @@ uType t_or_k origin orig_ty1 orig_ty2
         -- The arguments to 'go' are always semantically identical
         -- to orig_ty{1,2} except for looking through type synonyms
 
+     -- Unwrap casts before looking for variables. This way, we can easily
+     -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
+     -- didn't do it this way, and then the unification above was deferred.
+    go (CastTy t1 co1) t2
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
+
+    go t1 (CastTy t2 co2)
+      = do { co_tys <- uType t_or_k origin t1 t2
+           ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
+
         -- Variables; go for uVar
         -- Note that we pass in *original* (before synonym expansion),
         -- so that type variables tend to get filled in with
@@ -1326,14 +1337,6 @@ uType t_or_k origin orig_ty1 orig_ty2
       | tc1 == tc2
       = return $ mkNomReflCo ty1
 
-    go (CastTy t1 co1) t2
-      = do { co_tys <- go t1 t2
-           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
-
-    go t1 (CastTy t2 co2)
-      = do { co_tys <- go t1 t2
-           ; return ( mkCoherenceRightCo Nominal t2 co2 co_tys) }
-
         -- See Note [Expanding synonyms during unification]
         --
         -- Also NB that we recurse to 'go' so that we don't push a
index dd661a9..316f7eb 100644 (file)
@@ -15,3 +15,17 @@ T12634.hs:14:58: error:
       In the type signature:
         bench_twacePow :: forall t m m' r.
                           _ => t m' r -> Bench '(t, m, m', r)
+
+T12634.hs:15:18: error:
+    • Couldn't match kind ‘(* -> * -> *, *, *, *)’ with ‘*’
+      When matching types
+        params0 :: *
+        '(t, m, m', r) :: (* -> * -> *, *, *, *)
+      Expected type: t m' r -> Bench '(t, m, m', r)
+        Actual type: t m' r -> Bench params0
+    • In the expression: bench (twacePowDec :: t m' r -> t m r)
+      In an equation for ‘bench_twacePow’:
+          bench_twacePow = bench (twacePowDec :: t m' r -> t m r)
+    • Relevant bindings include
+        bench_twacePow :: t m' r -> Bench '(t, m, m', r)
+          (bound at T12634.hs:15:1)
index c0e0664..b931894 100644 (file)
@@ -1,41 +1,4 @@
 
-T14040a.hs:21:18: error:
-    • Couldn't match type ‘a’ with ‘k0’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x.
-                                                                x -> WeirdList x -> *).
-                           Sing wl
-                           -> (forall y. p k0 w0 'WeirdNil)
-                           -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                               Sing x
-                               -> Sing xs -> p (WeirdList k1) w1 xs -> p k1 w2 ('WeirdCons x xs))
-                           -> p k2 w3 wl
-        at T14040a.hs:(21,18)-(28,23)
-      Expected type: Sing wl
-                     -> (forall y. p k1 w0 'WeirdNil)
-                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x
-                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
-                     -> p k2 w3 wl
-        Actual type: Sing wl
-                     -> (forall y. p k1 w0 'WeirdNil)
-                     -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                         Sing x
-                         -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs))
-                     -> p k2 w3 wl
-    • In the ambiguity check for ‘elimWeirdList’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        elimWeirdList :: forall (a :: Type)
-                                (wl :: WeirdList a)
-                                (p :: forall (x :: Type). x -> WeirdList x -> Type).
-                         Sing wl
-                         -> (forall (y :: Type). p _ WeirdNil)
-                            -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
-                                Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-                               -> p _ wl
-
 T14040a.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
                                        -> (forall y. p k0 w0 'WeirdNil)
index c53c822..f4f1887 100644 (file)
@@ -1,26 +1,58 @@
 
 T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Could not deduce (SingI a) arising from a use of ‘sing’
+    • Could not deduce: m1 ~ Type
       from the context: (Action act, Monoid a, Good m1)
         bound by the instance declaration at T14584.hs:54:10-89
+      ‘m1’ is a rigid type variable bound by
+        the instance declaration
+        at T14584.hs:54:10-89
+      When matching types
+        a :: Type
+        a0 :: m
+      Expected type: Sing a0
+        Actual type: Sing a
     • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
       In the expression:
         act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
 
-T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Expected kind ‘m1’, but ‘a’ has kind ‘Type’
-    • In the type ‘a’
-      In the second argument of ‘fromSing’, namely
+T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce: a ~~ a0
+      from the context: (Action act, Monoid a, Good m1)
+        bound by the instance declaration at T14584.hs:54:10-89
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at T14584.hs:54:10-89
+      Expected type: Sing a0
+        Actual type: Sing a
+    • In the second argument of ‘fromSing’, namely
         ‘(sing @m @a :: Sing _)’
       In the fourth argument of ‘act’, namely
         ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
+    • Relevant bindings include
+        monHom :: a -> a (bound at T14584.hs:56:3)
+
+T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Could not deduce (SingI a) arising from a use of ‘sing’
+      from the context: (Action act, Monoid a, Good m1)
+        bound by the instance declaration at T14584.hs:54:10-89
+    • In the second argument of ‘fromSing’, namely
+        ‘(sing @m @a :: Sing _)’
+      In the fourth argument of ‘act’, namely
+        ‘(fromSing @m (sing @m @a :: Sing _))’
+      In the expression:
+        act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
 
 T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘a :: m’
-      Where: ‘a’, ‘m’ are rigid type variables bound by
+    • Found type wildcard ‘_’ standing for ‘a0 :: m’
+      Where: ‘a0’ is an ambiguous type variable
+             ‘m’ is a rigid type variable bound by
                the instance declaration
                at T14584.hs:54:10-89
     • In an expression type signature: Sing _
index 3e63159..43f7622 100644 (file)
@@ -10,7 +10,8 @@ T12593.hs:12:31: error:
     • Expecting one more argument to ‘k’
       Expected a type, but
       ‘k’ has kind
-      ‘(((k0 -> k1 -> *) -> Constraint) -> k2 -> *) -> Constraint’
+      ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+       -> Constraint’
     • In the kind ‘k’
       In the type signature:
         run :: k2 q =>
@@ -21,21 +22,65 @@ T12593.hs:12:40: error:
     • Expecting two more arguments to ‘k1’
       Expected a type, but
       ‘k1’ has kind
-      ‘((k0 -> k1 -> *) -> Constraint) -> k2 -> *’
+      ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
     • In the kind ‘k1’
       In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
 
-T12593.hs:12:54: error:
-    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) -> k2 -> *’
+T12593.hs:12:47: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k2 :: *
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+    • In the first argument of ‘p’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:49: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
+                     with ‘*’
+      When matching kinds
+        k3 :: *
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+    • In the second argument of ‘p’, namely ‘d’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:56: error:
+    • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
+                            -> (k2 -> k3 -> *) -> *)
+                           -> Constraint’
+                     with ‘*’
+      When matching kinds
+        k0 :: *
+        k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *)
+             -> Constraint
+    • In the first argument of ‘q’, namely ‘c’
+      In the type signature:
+        run :: k2 q =>
+               Free k k1 k2 p a b
+               -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
+
+T12593.hs:12:58: error:
+    • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
+                           -> (k2 -> k3 -> *) -> *’
                      with ‘*’
       When matching kinds
-        k3 :: ((k0 -> k1 -> *) -> Constraint) -> k2 -> *
         k1 :: *
-      Expected kind ‘k -> k3 -> *’, but ‘q’ has kind ‘k0 -> k1 -> *’
-    • In the type signature:
+        k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *
+    • In the second argument of ‘q’, namely ‘d’
+      In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
index 1bfa942..3abdb88 100644 (file)
@@ -3,11 +3,11 @@ T14846.hs:38:8: error:
     • Couldn't match type ‘ríki’ with ‘Hom riki’
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
-          i :: forall k5 (cls1 :: k5
-                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki :: Struct
-                                                                                             cls1
+          i :: forall k5 (cls2 :: k5
+                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls2) (ríki :: Struct
+                                                                                             cls2
                                                                                            -> Struct
-                                                                                                cls1
+                                                                                                cls2
                                                                                            -> *).
                StructI xx a =>
                ríki a a
@@ -30,11 +30,18 @@ T14846.hs:38:8: error:
                       ríki a a
       In the instance declaration for ‘Category (Hom riki)’
 
-T14846.hs:39:44: error:
-    • Expected kind ‘Struct cls0 -> Constraint’,
-        but ‘cls’ has kind ‘k4 -> Constraint’
-    • In the second argument of ‘Structured’, namely ‘cls’
-      In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
+T14846.hs:39:31: error:
+    • Couldn't match kind ‘k4’ with ‘Struct cls0’
+      ‘k4’ is a rigid type variable bound by
+        the instance declaration
+        at T14846.hs:37:10-65
+      When matching kinds
+        cls :: k4 -> Constraint
+        cls1 :: Struct cls0 -> Constraint
+      Expected kind ‘Struct cls1’,
+        but ‘Structured a cls’ has kind ‘Struct cls’
+    • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
       In an expression type signature: AStruct (Structured a cls)
+      In the expression: struct :: AStruct (Structured a cls)
     • Relevant bindings include
         i :: Hom riki a a (bound at T14846.hs:39:3)
index 4a9d3c0..5cf4fde 100644 (file)
@@ -20,11 +20,11 @@ T2494.hs:15:14: error:
         x :: Maybe a (bound at T2494.hs:14:65)
 
 T2494.hs:15:30: error:
-    • Couldn't match type ‘a’ with ‘b
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match type ‘b’ with ‘a
+      ‘b’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
-      ‘b’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the RULE "foo/foo"
         at T2494.hs:(12,1)-(15,33)
       Expected type: Maybe (m b) -> Maybe (m a)
index a995801..6cb1f44 100644 (file)
@@ -25,6 +25,17 @@ VtaFail.hs:26:15: error:
       In the expression: first @Int F
       In an equation for ‘fInt’: fInt = first @Int F
 
+VtaFail.hs:26:19: error:
+    • Couldn't match kind ‘*’ with ‘* -> *’
+      When matching types
+        a1 :: * -> *
+        Int :: *
+      Expected type: First Int
+        Actual type: First a1
+    • In the second argument of ‘first’, namely ‘F’
+      In the expression: first @Int F
+      In an equation for ‘fInt’: fInt = first @Int F
+
 VtaFail.hs:33:18: error:
     • Couldn't match type ‘Int’ with ‘Bool’
       Expected type: Proxy Bool
@@ -39,6 +50,17 @@ VtaFail.hs:40:17: error:
       In the expression: too @Maybe T
       In an equation for ‘threeBad’: threeBad = too @Maybe T
 
+VtaFail.hs:40:23: error:
+    • Couldn't match kind ‘*’ with ‘k0 -> *’
+      When matching types
+        a0 :: * -> k0 -> *
+        Maybe :: * -> *
+      Expected type: Three Maybe
+        Actual type: Three a0
+    • In the second argument of ‘too’, namely ‘T’
+      In the expression: too @Maybe T
+      In an equation for ‘threeBad’: threeBad = too @Maybe T
+
 VtaFail.hs:41:27: error:
     • Couldn't match type ‘Either’ with ‘(->)’
       Expected type: Three (->)