Injective type families

For details see #6018, Phab:D202 and the wiki page:

https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

This patch also wires-in Maybe data type and updates haddock submodule.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Subscribers: mpickering, bgamari, alanz, thomie, goldfire, simonmar,
             carter

Differential Revision: https://phabricator.haskell.org/D202

GHC Trac Issues: #6018

1 files changed, 149 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
new file mode 100644
index 0000000000..440ddacd91
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -0,0 +1,149 @@
+[1 of 5] Compiling T6018Bfail       ( T6018Bfail.hs, T6018Bfail.o )
+[2 of 5] Compiling T6018Dfail       ( T6018Dfail.hs, T6018Dfail.o )
+[3 of 5] Compiling T6018Cfail       ( T6018Cfail.hs, T6018Cfail.o )
+[4 of 5] Compiling T6018Afail       ( T6018Afail.hs, T6018Afail.o )
+[5 of 5] Compiling T6018fail        ( T6018fail.hs, T6018fail.o )
+
+T6018Afail.hs:7:15:
+    Type family equations violate injectivity annotation:
+      G Char Bool Int = Int
+      G Bool Int Char = Int
+
+T6018Dfail.hs:7:15:
+    Type family equations violate injectivity annotation:
+      T6018Bfail.H Bool Int Char = Int
+      T6018Bfail.H Char Bool Int = Int
+
+T6018fail.hs:13:15:
+    Type family equations violate injectivity annotation:
+      F Bool Int Char = Int
+      F Char Bool Int = Int
+
+T6018fail.hs:19:15:
+    Type family equations violate injectivity annotation:
+      I Int Int Int = Bool
+      I Int Char Bool = Bool
+
+T6018fail.hs:28:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      IdProxy a = Id a
+
+T6018fail.hs:36:15:
+    Type family equation violates 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
+
+T6018fail.hs:37:15:
+    Type family equations violate injectivity annotation:
+      P ('S n) m = 'S (P n m)
+      P 'Z m = m
+
+T6018fail.hs:42:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      J Int b c = Char
+
+T6018fail.hs:46:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘n’ does not appear on injective position.
+    In the RHS of type family equation:
+      K ('S n) m = 'S m
+
+T6018fail.hs:51:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      L a = MaybeSyn a
+
+T6018fail.hs:59:10:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVarsF '[] = '[]
+
+T6018fail.hs:62:15:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+      PolyKindVars '[] = '[]
+
+T6018fail.hs:66:15:
+    Type family equation violates injectivity annotation.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+    forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
+
+T6018fail.hs:70:15:
+    Type family equation violates injectivity annotation.
+    Injective type variables ‘a’, ‘b’ do not appear on injective position.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+    forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
+
+T6018fail.hs:75:15:
+    Type family equations violate injectivity annotation:
+      F1 (Maybe a) = Maybe (GF2 a)
+      F1 [a] = Maybe (GF1 a)
+
+T6018fail.hs:87:15:
+    Type family equation violates 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
+
+T6018fail.hs:90:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      W2 [a] = W2 a
+
+T6018fail.hs:95:15:
+    Type family equations violate injectivity annotation:
+      Z1 (Maybe b) = (b, [b])
+      Z1 [a] = (a, a)
+
+T6018fail.hs:99:15:
+    Type family equations violate injectivity annotation:
+      G1 (Maybe b) = [(b, b)]
+      G1 [a] = [a]
+
+T6018fail.hs:103:15:
+    Type family equations violate injectivity annotation:
+      G3 a Bool = (Bool, a)
+      G3 a Int = (a, Int)
+
+T6018fail.hs:106:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘b’ does not appear on injective position.
+    In the RHS of type family equation:
+      G4 a b = [a]
+
+T6018fail.hs:110:15:
+    Type family equations violate injectivity annotation:
+      G5 Int = [Bool]
+      G5 [a] = [GF1 a]
+
+T6018fail.hs:113:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘a’ does not appear on injective position.
+    In the RHS of type family equation:
+      G6 [a] = [HF1 a]
+
+T6018fail.hs:118:15:
+    Type family equation violates injectivity annotation.
+    Injective type variable ‘c’ does not appear on injective position.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
+    In the RHS of type family equation:
+    forall (k :: BOX) a b (c :: k). G7 a b c = [G7a a b c]
+
+T6018fail.hs:129:1:
+    Type family equations violate injectivity annotation:
+      FC Int Bool = Bool
+      FC Int Char = Bool
+
+T6018fail.hs:134:1:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation is a bare type variable
+    but these LHS type and kind patterns are not bare variables: ‘*’, ‘Char’
+      FC Char a = a