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

7 files changed, 355 insertions, 0 deletions

diff --git a/testsuite/tests/ghci/scripts/T6018ghci.script b/testsuite/tests/ghci/scripts/T6018ghci.script
new file mode 100644
index 0000000000..4615be2d04
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghci.script
@@ -0,0 +1,22 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+
+type family F a b c = (result :: k) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Char
+type instance F Bool Int  Char = Char
+
+type family I (a :: k) b (c :: k) = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Char Int  = Bool
+type instance I Bool Int  Int  = Int
+
+type family J a (b :: k) = r | r -> a
+type instance J Int b = Char
+
+type MaybeSyn a = Maybe a
+type family K a = r | r -> a
+type instance K a = MaybeSyn a
diff --git a/testsuite/tests/ghci/scripts/T6018ghci.stdout b/testsuite/tests/ghci/scripts/T6018ghci.stdout
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghci.stdout
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.script b/testsuite/tests/ghci/scripts/T6018ghcifail.script
new file mode 100644
index 0000000000..c0e073457f
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.script
@@ -0,0 +1,114 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+
+
+
+type family F a b c = (result :: *) | result -> a b c
+type instance F Int  Char Bool = Bool
+type instance F Char Bool Int  = Int
+type instance F Bool Int  Char = Int
+
+
+
+type family I a b c = r | r -> a b
+type instance I Int  Char Bool = Bool
+type instance I Int  Int  Int  = Bool
+type instance I Bool Int  Int  = Int
+
+-- Id is injective...
+type family Id a = result | result -> a
+type instance Id a = a
+
+-- ...but despite that we disallow a call to Id
+type family IdProxy a = r | r -> a
+type instance IdProxy a = Id a
+
+data N = Z | S N
+
+-- P is not injective, although the user declares otherwise. This
+-- should be rejected on the grounds of calling a type family in the
+-- RHS.
+type family P (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance P  Z    m = m
+type instance P (S n) m = S (P n m)
+
+-- this is not injective - not all injective type variables mentioned
+-- on LHS are mentioned on RHS
+type family J a b c = r | r -> a b
+type instance J Int b c = Char
+
+-- same as above, but tyvar is now nested inside a tycon
+type family K (a :: N) (b :: N) = (r :: N) | r -> a b
+type instance K (S n) m = S m
+
+-- Make sure we look through type synonyms to catch errors
+type MaybeSyn a = Id a
+type family L a = r | r -> a
+type instance L a = MaybeSyn a
+
+-- These should fail because given the RHS kind there is no way to determine LHS
+-- kind
+class PolyKindVarsC a where { type PolyKindVarsF a = (r :: k) | r -> a }
+
+instance PolyKindVarsC '[] where { type PolyKindVarsF '[] = '[] }
+
+
+
+type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
+type instance PolyKindVars '[] = '[]
+
+-- This should fail because there is no way to determine k from the RHS
+type family Fc (a :: k) (b :: k) = r | r -> k
+type instance Fc a b = Int
+
+-- This should fail because there is no way to determine a, b and k from the RHS
+type family Gc (a :: k) (b :: k) = r | r -> a b
+type instance Gc a b = Int
+
+type family GF1 a = r | r -> a
+type instance GF1 Int = Bool
+
+type family GF2 a = r | r -> a
+type instance GF2 Int = Bool
+
+type family HF1 a
+type instance HF1 Bool = Bool
+
+-- fails because injectivity is not compositional in this case
+type family F1 a = r | r -> a
+type instance F1 [a]       = Maybe (GF1 a)
+type instance F1 (Maybe a) = Maybe (GF2 a)
+
+type family W1 a = r | r -> a
+type instance W1 [a] = a
+
+type family W2 a = r | r -> a
+type instance W2 [a] = W2 a
+
+-- not injective because of infinite types
+type family Z1 a = r | r -> a
+type instance Z1 [a]       = (a, a)
+type instance Z1 (Maybe b) = (b, [b])
+
+type family G1 a = r | r -> a
+type instance G1 [a]       = [a]
+type instance G1 (Maybe b) = [(b, b)]
+
+type family G3 a b = r | r -> b
+type instance G3 a Int  = (a, Int)
+type instance G3 a Bool = (Bool, a)
+
+type family G4 a b = r | r -> a b
+type instance G4 a b = [a]
+
+type family G5 a = r | r -> a
+type instance G5 [a] = [GF1 a] -- GF1 injective
+type instance G5 Int = [Bool]
+
+type family G6 a = r | r -> a
+type instance G6 [a]  = [HF1 a] -- HF1 not injective
+type instance G6 Bool = Int
+
+
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
new file mode 100644
index 0000000000..e1c0055349
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -0,0 +1,111 @@
+
+<interactive>:10:15:
+    Type family equations violate injectivity annotation:
+      F Char Bool Int = Int
+      F Bool Int Char = Int
+
+<interactive>:16:15:
+    Type family equations violate injectivity annotation:
+      I Int Char Bool = Bool
+      I Int Int Int = Bool
+
+<interactive>:26:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      IdProxy a = Id a
+
+<interactive>:34: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
+
+<interactive>:40: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
+
+<interactive>:44: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
+
+<interactive>:49:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      L a = MaybeSyn a
+
+<interactive>:55:41:
+    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 '[] = '[]
+
+<interactive>:60: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 '[] = '[]
+
+<interactive>:64: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
+
+<interactive>:68: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
+
+<interactive>:81:15:
+    Type family equations violate injectivity annotation:
+      F1 [a] = Maybe (GF1 a)
+      F1 (Maybe a) = Maybe (GF2 a)
+
+<interactive>:85: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
+
+<interactive>:88:15:
+    Type family equation violates injectivity annotation.
+    RHS of injective type family equation cannot be a type family:
+      W2 [a] = W2 a
+
+<interactive>:92:15:
+    Type family equations violate injectivity annotation:
+      Z1 [a] = (a, a)
+      Z1 (Maybe b) = (b, [b])
+
+<interactive>:96:15:
+    Type family equations violate injectivity annotation:
+      G1 [a] = [a]
+      G1 (Maybe b) = [(b, b)]
+
+<interactive>:100:15:
+    Type family equations violate injectivity annotation:
+      G3 a Int = (a, Int)
+      G3 a Bool = (Bool, a)
+
+<interactive>:104: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]
+
+<interactive>:107:15:
+    Type family equations violate injectivity annotation:
+      G5 [a] = [GF1 a]
+      G5 Int = [Bool]
+
+<interactive>:111: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]
diff --git a/testsuite/tests/ghci/scripts/T6018ghcirnfail.script b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
new file mode 100644
index 0000000000..f1a5fa469a
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcirnfail.script
@@ -0,0 +1,42 @@
+:set -XTypeFamilies
+:set -XDataKinds
+:set -XUndecidableInstances
+:set -XPolyKinds
+:set -XMultiParamTypeClasses
+
+-- IA = injectivity annotation `| foo -> bar`
+
+-- use incorrect tyvar in LHS of IA
+type family F a = r | a -> a
+type family Fc a = r | a -> a where { Fc a = a }
+class Fcl a where { type Ft a = r | a -> a }
+
+-- declare result tyvar to be duplicate (without IA)
+type family G a = a
+type family Gc a = a where { Gc a = a }
+
+-- declare result tyvar to be duplicate (with IA)
+type family Gb a = a | a -> a
+type family Gcb a = a | a -> a where { Gcb a = a }
+class Gclb a where { type Gtb a = a | a -> a } -- here we want two errors
+
+-- not in-scope tyvar in RHS of IA
+type family I a b = r | r -> c
+type family Ic a b = r | r -> c where { Ic a b = a }
+class Icl a b where { type It a b = r | r -> c }
+
+-- repeated tyvar on RHS of IA
+type family J a b = r | r -> a a
+type family Jc a b = r | r -> a a where { Jc a b = a }
+class Jcl a b where { type Jt a b = r | r -> a a }
+
+-- not in-scope tyvar in LHS of IA
+type family L a b = r | c -> a
+type family Lc a b = r | c -> a where { Lc a b = a }
+class Lcl a b where { type Lt a b = r | c -> a }
+
+-- result variable shadows variable in class head
+class M a b where { type Mt b = a | a -> b }
+
+-- here b is out-of-scope
+class N a b where { type Nt a = r | r -> a b }
diff --git a/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr b/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr
new file mode 100644
index 0000000000..87f5a040b1
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T6018ghcirnfail.stderr
@@ -0,0 +1,63 @@
+
+<interactive>:10:23:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:11:24:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:12:37:
+    Incorrect type variable on the LHS of injectivity condition
+         Expected : r
+         Actual   : a
+
+<interactive>:15:19:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:16:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:19:20:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:19:24:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:20:21:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:20:25:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:21:35:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:21:39:
+    Unknown type variable on the RHS of injectivity condition: a
+
+<interactive>:24:1: Not in scope: type variable ‘c’
+
+<interactive>:25:1: Not in scope: type variable ‘c’
+
+<interactive>:26:23: Not in scope: type variable ‘c’
+
+<interactive>:34:1: Not in scope: type variable ‘c’
+
+<interactive>:35:1: Not in scope: type variable ‘c’
+
+<interactive>:36:23: Not in scope: type variable ‘c’
+
+<interactive>:39:33:
+    Type variable ‘a’, naming a type family result,
+    shadows an already bound type variable
+
+<interactive>:42:37:
+    Unknown type variable on the RHS of injectivity condition: b
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index bbd69ee014..d2244c1790 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -161,6 +161,9 @@ test('T7627', normal, ghci_script, ['T7627.script'])
 test('T7627b', normal, ghci_script, ['T7627b.script'])
 test('T7586', normal, ghci_script, ['T7586.script'])
 test('T4175', normal, ghci_script, ['T4175.script'])
+test('T6018ghci', normal, ghci_script, ['T6018ghci.script'])
+test('T6018ghcifail', normal, ghci_script, ['T6018ghcifail.script'])
+test('T6018ghcirnfail', normal, ghci_script, ['T6018ghcirnfail.script'])
 test('T7730', combined_output, ghci_script, ['T7730.script'])
 test('T7872', normal, ghci_script, ['T7872.script'])
 test('T7873', normal, ghci_script, ['T7873.script'])