From 73a7383ebc17f495d7acd04007c8c56b46532cb6 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Tue, 21 Jan 2020 17:52:48 +0000 Subject: 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. --- testsuite/tests/dependent/should_fail/T14066e.stderr | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'testsuite/tests/dependent/should_fail/T14066e.stderr') 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) -- cgit v1.2.1