Commit 042df603 authored by Richard Eisenberg's avatar Richard Eisenberg

Unwrap casts before checking vars in eager unifier

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.
parent 8ec29460
......@@ -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
......
......@@ -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)
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)
......
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 _
......
......@@ -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
......@@ -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)
......@@ -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)
......
......@@ -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 (->)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment