From 55ca10855713f3cc14b17f1b67f14c36dea4c651 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Thu, 7 Nov 2019 17:56:16 +0000 Subject: Fix #17405 by not checking imported equations Previously, we checked all imported type family equations for injectivity. This is very silly. Now, we check only for conflicts. Before I could even imagine doing the fix, I needed to untangle several functions that were (in my opinion) overly complicated. It's still not quite as perfect as I'd like, but it's good enough for now. Test case: typecheck/should_compile/T17405 --- testsuite/tests/ghci/scripts/T6018ghcifail.stderr | 47 +++++++++++++---------- 1 file changed, 27 insertions(+), 20 deletions(-) (limited to 'testsuite/tests/ghci/scripts') diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr index b171221e17..bbea2d4398 100644 --- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr +++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr @@ -1,44 +1,46 @@ :10:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: F Char Bool Int = Int -- Defined at :10:15 F Bool Int Char = Int -- Defined at :11:15 :16:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: I Int Char Bool = Bool -- Defined at :16:15 I Int Int Int = Bool -- Defined at :17:15 :26:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. RHS of injective type family equation cannot be a type family: IdProxy a = Id a -- Defined at :26:15 :34:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. RHS of injective type family equation is a bare type variable but these LHS type and kind patterns are not bare variables: ‘'Z’ P 'Z m = m -- Defined at :34:15 :40:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type variable ‘b’ cannot be inferred from the right-hand side. In the type family equation: J Int b c = Char -- Defined at :40:15 :44:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type variable ‘n’ cannot be inferred from the right-hand side. In the type family equation: K ('S n) m = 'S m -- Defined at :44:15 :49:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. RHS of injective type family equation cannot be a type family: L a = MaybeSyn a -- Defined at :49:15 :55:41: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type/kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: @@ -46,7 +48,7 @@ -- Defined at :55:41 :60:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type/kind variable ‘k1’ cannot be inferred from the right-hand side. In the type family equation: @@ -54,14 +56,14 @@ -- Defined at :60:15 :64:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type/kind variable ‘k’ cannot be inferred from the right-hand side. In the type family equation: forall k (a :: k) (b :: k). Fc @k a b = Int -- Defined at :64:15 :68:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type/kind variables ‘k’, ‘a’, ‘b’ cannot be inferred from the right-hand side. In the type family equation: @@ -69,49 +71,54 @@ Gc @k a b = Int -- Defined at :68:15 :81:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: F1 [a] = Maybe (GF1 a) -- Defined at :81:15 F1 (Maybe a) = Maybe (GF2 a) -- Defined at :82:15 :85:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. RHS of injective type family equation is a bare type variable but these LHS type and kind patterns are not bare variables: ‘[a]’ W1 [a] = a -- Defined at :85:15 :88:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. RHS of injective type family equation cannot be a type family: W2 [a] = W2 a -- Defined at :88:15 :92:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: Z1 [a] = (a, a) -- Defined at :92:15 Z1 (Maybe b) = (b, [b]) -- Defined at :93:15 :96:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: G1 [a] = [a] -- Defined at :96:15 G1 (Maybe b) = [(b, b)] -- Defined at :97:15 :100:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: G3 a Int = (a, Int) -- Defined at :100:15 G3 a Bool = (Bool, a) -- Defined at :101:15 :104:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type variable ‘b’ cannot be inferred from the right-hand side. In the type family equation: G4 a b = [a] -- Defined at :104:15 :107:15: error: - Type family equations violate injectivity annotation: + Type family equation right-hand sides overlap; this violates + the family's injectivity annotation: G5 [a] = [GF1 a] -- Defined at :107:15 G5 Int = [Bool] -- Defined at :108:15 :111:15: error: - Type family equation violates injectivity annotation. + Type family equation violates the family's injectivity annotation. Type variable ‘a’ cannot be inferred from the right-hand side. In the type family equation: G6 [a] = [HF1 a] -- Defined at :111:15 -- cgit v1.2.1