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/patsyn | |
| 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/patsyn')
| -rw-r--r-- | testsuite/tests/patsyn/should_fail/T15685.stderr | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr index 13fc5a81ec..7f01ebc479 100644 --- a/testsuite/tests/patsyn/should_fail/T15685.stderr +++ b/testsuite/tests/patsyn/should_fail/T15685.stderr @@ -1,9 +1,21 @@ T15685.hs:13:24: error: - • Kind mismatch: cannot unify (f :: a -> *) with: + • Couldn't match kind ‘a1’ with ‘[k0]’ + ‘a1’ is untouchable + inside the constraints: as ~ (a2 : as1) + bound by a pattern with constructor: + Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]). + f a2 -> NS f (a2 : as), + in a pattern synonym declaration + at T15685.hs:13:19-26 + ‘a1’ is a rigid type variable bound by + the inferred type of HereNil :: NS f as + at T15685.hs:13:9-15 + Possible fix: add a type signature for ‘HereNil’ + When matching types + f :: a1 -> * NP a0 :: [k0] -> * - Their kinds differ. - Expected type: f a1 + Expected type: f a2 Actual type: NP a0 b0 • In the pattern: Nil In the pattern: Here Nil |