diff options
author | Richard Eisenberg <rae@richarde.dev> | 2020-01-21 17:52:48 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-03-20 20:42:56 -0400 |
commit | 73a7383ebc17f495d7acd04007c8c56b46532cb6 (patch) | |
tree | b3c9cabb3dc8ae0e7808fda0d65fa8696ebe1570 /testsuite/tests/typecheck/should_fail/T15629.stderr | |
parent | cb1785d9f839e34a3a4892f354f0c51cc6553c0e (diff) | |
download | haskell-73a7383ebc17f495d7acd04007c8c56b46532cb6.tar.gz |
Simplify treatment of heterogeneous equality
Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.
The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.
All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.
There are a few knock-on effects, documented where they occur.
While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.
This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.
Diffstat (limited to 'testsuite/tests/typecheck/should_fail/T15629.stderr')
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15629.stderr | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr index a0e0f42286..ac307ed9d5 100644 --- a/testsuite/tests/typecheck/should_fail/T15629.stderr +++ b/testsuite/tests/typecheck/should_fail/T15629.stderr @@ -1,7 +1,7 @@ T15629.hs:26:37: error: • Expected kind ‘x1 ~> F x1 ab1’, - but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z’ + but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z1’ • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’ In the first argument of ‘Proxy’, namely ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’ @@ -10,18 +10,18 @@ T15629.hs:26:37: error: Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) T15629.hs:27:9: error: - • Couldn't match kind ‘ab1’ with ‘z’ - ‘ab1’ is a rigid type variable bound by + • Couldn't match kind ‘z1’ with ‘ab1’ + ‘z1’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) at T15629.hs:26:5-84 - ‘z’ is a rigid type variable bound by + ‘ab1’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) at T15629.hs:26:5-84 When matching types f0 :: x ~> F x ab - F1Sym :: TyFun x1 (F x1 z) -> * + F1Sym :: TyFun x1 (F x1 z1) -> * Expected type: Proxy (Comp F1Sym F2Sym) Actual type: Proxy (Comp f0 F2Sym) • In the expression: sg Proxy Proxy |