Allow associated types to pattern-match in non-class-bound variables

Summary:
After 8136a5cbfcd24647f897a2fae9fcbda0b1624035 (#11450), if you have
a class with an associated type:

```
class C a where
  type T a b
```

And you try to create an instance of `C` like this:

```
instance C Int where
  type T Int Char = Bool
```

Then it is rejected, since you're trying to instantiate the variable ``b`` with
something other than a type variable. But this restriction proves quite
onerous in practice, as it prevents you from doing things like this:

```
class C a where
  type T a (b :: Identity c) :: c

instance C Int where
  type T Int ('Identity x) = x
```

You have to resort to an auxiliary type family in order to define this now,
which becomes extremely tiring. This lifts this restriction and fixes #13398,
in which it was discovered that adding this restriction broke code in the wild.

Test Plan: ./validate

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: rwbarton, thomie

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

15 files changed, 125 insertions, 114 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 0dd5af3f95..a56e7a2418 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1416,7 +1416,7 @@ With this class decl, if we have an instance decl
   instance C ty1 ty2 where ...
 then the type instance must look like
      type T ty1 v ty2 = ...
-with exactly 'ty1' for 'a', 'ty2' for 'b', and a variable for 'x'.
+with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
 For example:
 
   instance C [p] Int
@@ -1443,20 +1443,40 @@ Note that
   on the LHS to establish the repeated pattern.  So to keep it simple
   we just require equality.
 
-* We also check that any non-class-tyvars are instantiated with
-  distinct tyvars.  That rules out
+* For variables in associated type families that are not bound by the class
+  itself, we do _not_ check if they are over-specific. In other words,
+  it's perfectly acceptable to have an instance like this:
+
     instance C [p] Int where
-      type T [p] Bool Int = p  -- Note Bool
-      type T [p] Char Int = p  -- Note Char
+      type T [p] (Maybe x) Int = x
+
+  While the first and third arguments to T are required to be exactly [p] and
+  Int, respectively, since they are bound by C, the second argument is allowed
+  to be more specific than just a type variable. Furthermore, it is permissible
+  to define multiple equations for T that differ only in the non-class-bound
+  argument:
 
-  and
-     instance C [p] Int where
-      type T [p] p Int = p     -- Note repeated 'p' on LHS
-  It's consistent to do this because we don't allow this kind of
-  instantiation for the class-tyvar arguments of the family.
+    instance C [p] Int where
+      type T [p] (Maybe x)    Int = x
+      type T [p] (Either x y) Int = x -> y
 
-  Overall, we can have exactly one type instance for each
-  associated type.  If you wantmore, use an auxiliary family.
+  We once considered requiring that non-class-bound variables in associated
+  type family instances be instantiated with distinct type variables. However,
+  that requirement proved too restrictive in practice, as there were examples
+  of extremely simple associated type family instances that this check would
+  reject, and fixing them required tiresome boilerplate in the form of
+  auxiliary type families. For instance, you would have to define the above
+  example as:
+
+    instance C [p] Int where
+      type T [p] x Int = CAux x
+
+    type family CAux x where
+      CAux (Maybe x)    = x
+      CAux (Either x y) = x -> y
+
+  We decided that this restriction wasn't buying us much, so we opted not
+  to pursue that design (see also GHC Trac #13398).
 
 Implementation
   * Form the mini-envt from the class type variables a,b
@@ -1466,7 +1486,8 @@ Implementation
     (it shares tyvars with the class C)
 
   * Apply the mini-evnt to them, and check that the result is
-    consistent with the instance types [p] y Int
+    consistent with the instance types [p] y Int. (where y can be any type, as
+    it is not scoped over the class type variables.
 
 We make all the instance type variables scope over the
 type instances, of course, which picks up non-obvious kinds.  Eg
@@ -1516,13 +1537,10 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
 
        -- Check type args first (more comprehensible)
        ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
-       ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars
 
        -- And now kind args
        ; checkTc (all check_arg kind_shapes)
                  (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
-       ; checkTc (check_poly_args kind_shapes)
-                 (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds)
 
        ; traceTc "cfi" (vcat [ ppr inst_tvs
                              , ppr arg_shapes
@@ -1538,21 +1556,11 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
     check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
     check_arg (Nothing,     _    ) = True -- Arg position does not correspond
                                           -- to a class variable
-    check_poly_args :: [(Maybe Type,Type)] -> Bool
-    check_poly_args arg_shapes
-      = allDistinctTyVars (mkVarSet inst_tvs)
-                          [ at_ty | (Nothing, at_ty) <- arg_shapes ]
 
     pp_wrong_at_arg
       = vcat [ text "Type indexes must match class instance head"
              , pp_exp_act ]
 
-    pp_wrong_at_tyvars
-      = vcat [ text "Polymorphic type indexes of associated type" <+> quotes (ppr fam_tc)
-             , nest 2 $ vcat [ text "(i.e. ones independent of the class type variables)"
-                             , text "must be distinct type variables" ]
-             , pp_exp_act ]
-
     pp_exp_act
       = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
              , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
diff --git a/docs/users_guide/8.2.1-notes.rst b/docs/users_guide/8.2.1-notes.rst
index 9a7236b42b..7d87ad3518 100644
--- a/docs/users_guide/8.2.1-notes.rst
+++ b/docs/users_guide/8.2.1-notes.rst
@@ -177,6 +177,25 @@ Compiler
 
   See :ghc-ticket:`13267`.
 
+- Validity checking for associated type family instances has tightened
+  somewhat. Before, this would be accepted: ::
+
+    class Foo a where
+      type Bar a
+
+    instance Foo (Either a b) where
+      type Bar (Either c d) = d -> c
+
+  This is now disallowed, as the type variables used in the `Bar` instance do
+  not match those in the instance head. This instance can be fixed by changing
+  it to: ::
+
+    instance Foo (Either a b) where
+      type Bar (Either a b) = b -> a
+
+  See the section on `associated type family instances <assoc-data-inst>` for
+  more information.
+
 GHCi
 ~~~~
 
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index c6f7f5ec3f..0e8e9563cf 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -7092,38 +7092,20 @@ keyword in the family instance: ::
       ...
 
 The data or type family instance for an assocated type must follow
-the following two rules:
+the rule that the type indexes corresponding to class parameters must have
+precisely the same as type given in the instance head. For example: ::
 
--  The type indexes corresponding to class parameters must have
-   precisely the same as type given in the instance head.
-   For example: ::
-
-       class Collects ce where
-         type Elem ce :: *
-
-       instance Eq (Elem [e]) => Collects [e] where
-         -- Choose one of the following alternatives:
-         type Elem [e] = e       -- OK
-         type Elem [x] = x       -- BAD; '[x]' is differnet to '[e]' from head
-         type Elem x   = x       -- BAD; 'x' is different to '[e]'
-         type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]'
-
--  The type indexes of the type family that do *not* correspond to
-   class parameters must be distinct type variables, not mentioned
-   in the instance head.  For example: ::
-
-       class C b x where
-          type F a b c :: *
+    class Collects ce where
+      type Elem ce :: *
 
-       instance C [v] [w] where
-         -- Choose one of the following alternatives:
-         type C a [v] c = a->c  -- OK; a,c are tyvars
-         type C x [v] y = y->x  -- OK; x,y are tyvars
-         type C x [v] x = x     -- BAD: x is repeated
-         type C x [v] w = x     -- BAD: w is mentioned in instance head
+    instance Eq (Elem [e]) => Collects [e] where
+      -- Choose one of the following alternatives:
+      type Elem [e] = e       -- OK
+      type Elem [x] = x       -- BAD; '[x]' is differnet to '[e]' from head
+      type Elem x   = x       -- BAD; 'x' is different to '[e]'
+      type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]'
 
-The effect of these two rules is that the type-family instance
-completely covers the cases covered by the instance head.
+Note the following points:
 
 -  An instance for an associated family can only appear as part of an
    instance declarations of the class in which the family was declared,
@@ -7138,9 +7120,9 @@ completely covers the cases covered by the instance head.
    inhabited; i.e., only diverging expressions, such as ``undefined``,
    can assume the type.
 
--  A historical note.  In the past (but no longer), GHC allowed you to
-   write *multiple* type or data family instances for a single
-   associated type.  For example: ::
+-  Although it is unusual, there (currently) can be *multiple* instances
+   for an associated family in a single instance declaration. For
+   example, this is legitimate: ::
 
        instance GMapKey Flob where
          data GMap Flob [v] = G1 v
@@ -7149,23 +7131,9 @@ completely covers the cases covered by the instance head.
 
    Here we give two data instance declarations, one in which the last
    parameter is ``[v]``, and one for which it is ``Int``. Since you
-   cannot give any *subsequent* instances for ``(GMap Flob ...)``,
-   this facility was not very useful, except perhaps when the free
-   indexed parameter has a fixed number of alternatives
-   (e.g. ``Bool``). But in that case it is better to define an auxiliary
-   closed type function like this: ::
-
-       class C a where
-         type F a (b :: Bool) :: *
-
-       instance C Int where
-         type F Int b = FInt b
-
-       type family FInt a b where
-         FInt True  = Char
-         FInt False = Bool
-
-    Here the auxiliary type function is ``FInt``.
+   cannot give any *subsequent* instances for ``(GMap Flob ...)``, this
+   facility is most useful when the free indexed parameter is of a kind
+   with a finite number of alternatives (unlike ``*``).
 
 .. _assoc-decl-defs:
 
diff --git a/testsuite/tests/ghci/scripts/T4175.hs b/testsuite/tests/ghci/scripts/T4175.hs
index 0b7b554062..0fc53e76e9 100644
--- a/testsuite/tests/ghci/scripts/T4175.hs
+++ b/testsuite/tests/ghci/scripts/T4175.hs
@@ -16,10 +16,10 @@ class C a where
     type D a b
 
 instance C Int where
-    type D Int b = String
+    type D Int () = String
 
 instance C () where
-    type D () a = Bool
+    type D () () = Bool
 
 type family E a where
     E ()  = Bool
diff --git a/testsuite/tests/ghci/scripts/T4175.stdout b/testsuite/tests/ghci/scripts/T4175.stdout
index fff1b150e5..6f56a5f868 100644
--- a/testsuite/tests/ghci/scripts/T4175.stdout
+++ b/testsuite/tests/ghci/scripts/T4175.stdout
@@ -9,8 +9,8 @@ data instance B () = MkB 	-- Defined at T4175.hs:13:15
 class C a where
   type family D a b :: *
   	-- Defined at T4175.hs:16:5
-type instance D () a = Bool 	-- Defined at T4175.hs:22:10
-type instance D Int b = String 	-- Defined at T4175.hs:19:10
+type instance D () () = Bool 	-- Defined at T4175.hs:22:10
+type instance D Int () = String 	-- Defined at T4175.hs:19:10
 type family E a :: *
   where
       E () = Bool
@@ -25,7 +25,8 @@ instance Show () -- Defined in ‘GHC.Show’
 instance Read () -- Defined in ‘GHC.Read’
 instance Enum () -- Defined in ‘GHC.Enum’
 instance Bounded () -- Defined in ‘GHC.Enum’
-type instance D () a = Bool 	-- Defined at T4175.hs:22:10
+type instance D () () = Bool 	-- Defined at T4175.hs:22:10
+type instance D Int () = String 	-- Defined at T4175.hs:19:10
 data instance B () = MkB 	-- Defined at T4175.hs:13:15
 data Maybe a = Nothing | Just a 	-- Defined in ‘GHC.Base’
 instance Applicative Maybe -- Defined in ‘GHC.Base’
@@ -50,7 +51,7 @@ instance Num Int -- Defined in ‘GHC.Num’
 instance Real Int -- Defined in ‘GHC.Real’
 instance Bounded Int -- Defined in ‘GHC.Enum’
 instance Integral Int -- Defined in ‘GHC.Real’
-type instance D Int b = String 	-- Defined at T4175.hs:19:10
+type instance D Int () = String 	-- Defined at T4175.hs:19:10
 type instance A Int Int = () 	-- Defined at T4175.hs:8:15
 class Z a 	-- Defined at T4175.hs:28:1
 instance F (Z a) -- Defined at T4175.hs:31:10
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index c5037a1f58..9765244f1e 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -38,14 +38,11 @@
       L a = MaybeSyn a -- Defined at <interactive>:49:15
 
 <interactive>:55:41: error:
-    • Polymorphic type indexes of associated type ‘PolyKindVarsF’
-        (i.e. ones independent of the class type variables)
-        must be distinct type variables
-      Expected: PolyKindVarsF '[]
-        Actual: PolyKindVarsF '[]
-      Use -fprint-explicit-kinds to see the kind arguments
-    • In the type instance declaration for ‘PolyKindVarsF’
-      In the instance declaration for ‘PolyKindVarsC '[]’
+    Type family equation violates injectivity annotation.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Use -fprint-explicit-kinds to see the kind arguments
+    In the type family equation:
+      PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
diff --git a/testsuite/tests/indexed-types/should_compile/T13398a.hs b/testsuite/tests/indexed-types/should_compile/T13398a.hs
new file mode 100644
index 0000000000..7d147eb8d5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T13398a.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T13398a where
+
+data Nat
+data Rate
+data StaticTicks where
+        (:/:) :: Nat -> Rate -> StaticTicks
+type ticks :/ rate = ticks ':/: rate
+
+class HasStaticDuration (s :: k) where
+  type SetStaticDuration s (pt :: StaticTicks) :: k
+
+instance HasStaticDuration (t :/ r) where
+  type SetStaticDuration (t :/ r) (t' :/ r') = t' :/ r'
diff --git a/testsuite/tests/indexed-types/should_compile/T13398b.hs b/testsuite/tests/indexed-types/should_compile/T13398b.hs
new file mode 100644
index 0000000000..0689ef39d6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T13398b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T13398b where
+
+import GHC.TypeLits
+
+class C a where
+  type T a (b :: Bool) :: a
+
+instance C Nat where
+  type T Nat 'True  = 1
+  type T Nat 'False = 0
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 66f8c5686c..529f7defda 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -261,3 +261,5 @@ test('T12676', normal, compile, [''])
 test('T12526', normal, compile, [''])
 test('T12538', normal, compile_fail, [''])
 test('T13244', normal, compile, [''])
+test('T13398a', normal, compile, [''])
+test('T13398b', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
index 57a9595254..4bd7bde8df 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
@@ -8,7 +8,6 @@ class C8 a where
 instance C8 Int where
   data S8 Int a = S8Int a
 
--- Extra argument is not a variable;
--- this is now not allowed
+-- Extra argument is not a variable; this is fine
 instance C8 Bool where
   data S8 Bool Char = S8Bool
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr
deleted file mode 100644
index 9b99cd1322..0000000000
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr
+++ /dev/null
@@ -1,11 +0,0 @@
-
-SimpleFail10.hs:14:3: error:
-    • Polymorphic type indexes of associated type ‘S8’
-        (i.e. ones independent of the class type variables)
-        must be distinct type variables
-      Expected: S8 Bool <tv>
-      Actual:   S8 Bool Char
-      where the `<tv>' arguments are type variables,
-      distinct from each other and from the instance variables
-    • In the data instance declaration for ‘S8’
-      In the instance declaration for ‘C8 Bool’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index d2833603ca..cca1e8dcad 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -10,7 +10,7 @@ test('SimpleFail6', normal, compile_fail, [''])
 test('SimpleFail7', normal, compile_fail, [''])
 test('SimpleFail8', normal, compile_fail, [''])
 test('SimpleFail9', normal, compile_fail, [''])
-test('SimpleFail10', normal, compile_fail, [''])
+test('SimpleFail10', normal, compile, [''])
 test('SimpleFail11a', normal, compile_fail, [''])
 test('SimpleFail11b', normal, compile_fail, [''])
 test('SimpleFail11c', normal, compile_fail, [''])
diff --git a/testsuite/tests/th/T9692.hs b/testsuite/tests/th/T9692.hs
index 3f67b0dee9..770290d7db 100644
--- a/testsuite/tests/th/T9692.hs
+++ b/testsuite/tests/th/T9692.hs
@@ -8,7 +8,7 @@ import Language.Haskell.TH.Ppr
 import System.IO
 
 class C a where
-        data F a b :: *
+        data F a (b :: k) :: *
 
 instance C Int where
         data F Int x = FInt x
diff --git a/testsuite/tests/th/T9692.stderr b/testsuite/tests/th/T9692.stderr
index f99d12bd74..ffa55365d4 100644
--- a/testsuite/tests/th/T9692.stderr
+++ b/testsuite/tests/th/T9692.stderr
@@ -1,2 +1,2 @@
-data family T9692.F (a_0 :: k_1) (b_2 :: *) :: *
-data instance T9692.F GHC.Types.Int x_3 = T9692.FInt x_3
+data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: *
+data instance T9692.F GHC.Types.Int (x_4 :: *) = T9692.FInt x_4
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index e3fe13ada5..8c7a273ed8 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -58,14 +58,11 @@ T6018fail.hs:51:15: error:
       L a = MaybeSyn a -- Defined at T6018fail.hs:51:15
 
 T6018fail.hs:59:10: error:
-    • Polymorphic type indexes of associated type ‘PolyKindVarsF’
-        (i.e. ones independent of the class type variables)
-        must be distinct type variables
-      Expected: PolyKindVarsF '[]
-        Actual: PolyKindVarsF '[]
-      Use -fprint-explicit-kinds to see the kind arguments
-    • In the type instance declaration for ‘PolyKindVarsF’
-      In the instance declaration for ‘PolyKindVarsC '[]’
+    Type family equation violates injectivity annotation.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Use -fprint-explicit-kinds to see the kind arguments
+    In the type family equation:
+      PolyKindVarsF '[] = '[] -- Defined at T6018fail.hs:59:10
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.