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/dependent | |
| 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/dependent')
| -rw-r--r-- | testsuite/tests/dependent/should_fail/BadTelescope5.stderr | 2 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T14066.stderr | 2 | ||||
| -rw-r--r-- | testsuite/tests/dependent/should_fail/T14066e.stderr | 18 |
3 files changed, 6 insertions, 16 deletions
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr index da79678d5b..57b2ee7876 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr @@ -1,6 +1,6 @@ BadTelescope5.hs:10:81: error: - • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’ + • Expected kind ‘k1’, but ‘d’ has kind ‘Proxy a1’ • In the second argument of ‘SameKind’, namely ‘d’ In the type signature: bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr index e5179e510b..a6780ff75f 100644 --- a/testsuite/tests/dependent/should_fail/T14066.stderr +++ b/testsuite/tests/dependent/should_fail/T14066.stderr @@ -1,6 +1,6 @@ T14066.hs:15:59: error: - • Expected kind ‘k’, but ‘b’ has kind ‘k1’ + • Expected kind ‘k2’, but ‘b’ has kind ‘k3’ • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: g :: forall k (b :: k). SameKind a b In the expression: diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index 03a2b9255d..ee903d6b4c 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,20 +1,10 @@ -T14066e.hs:13:59: error: - • Couldn't match kind ‘k’ with ‘*’ - ‘k’ is a rigid type variable bound by - the type signature for: - j :: forall {k} {k1} (c :: k) (b :: k1). - Proxy a -> Proxy b -> Proxy c -> Proxy b - at T14066e.hs:12:5-61 - When matching kinds - k1 :: * - c :: k - Expected kind ‘c’, but ‘b'’ has kind ‘k1’ - • In the first argument of ‘Proxy’, namely ‘(b' :: c')’ +T14066e.hs:13:65: error: + • Expected a type, but ‘c'’ has kind ‘k1’ + • In the kind ‘c'’ + In the first argument of ‘Proxy’, namely ‘(b' :: c')’ In an expression type signature: Proxy (b' :: c') - In the expression: p1 :: Proxy (b' :: c') • Relevant bindings include p2 :: Proxy c (bound at T14066e.hs:13:27) - p1 :: Proxy b (bound at T14066e.hs:13:10) j :: Proxy a -> Proxy b -> Proxy c -> Proxy b (bound at T14066e.hs:13:5) |