Commit 67345ccf authored by Ryan Scott's avatar Ryan Scott
Browse files

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

Summary:
After 8136a5cb (#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
parent b335f506
......@@ -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)
......
......@@ -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
~~~~
......
......@@ -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:
......
......@@ -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
......
......@@ -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
......@@ -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.
......
{-# 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'
{-# 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
......@@ -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, [''])
......@@ -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
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’
......@@ -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, [''])
......
......@@ -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
......
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
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment