Associated type family instance validity checking is too conservative

mediabus-0.3.0.1 currently fails to build on GHC HEAD because of this regression. Here's a simplified program which exemplifies the issue:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Mediabus 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'

This compiles fine on GHC 8.0.2, but on GHC HEAD, it gives an odd error:

$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.1.20170307: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Mediabus         ( Bug.hs, interpreted )

Bug.hs:19:8: error:
    • Polymorphic type indexes of associated type ‘SetStaticDuration’
        (i.e. ones independent of the class type variables)
        must be distinct type variables
      Expected: SetStaticDuration (t :/ r) <tv>
        Actual: SetStaticDuration (t :/ r) (t' :/ r')
      where the `<tv>' arguments are type variables,
      distinct from each other and from the instance variables
    • In the type instance declaration for ‘SetStaticDuration’
      In the instance declaration for ‘HasStaticDuration (t :/ r)’
   |
19 |   type SetStaticDuration (t :/ r) (t' :/ r') = t' :/ r'
   |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This error message comes from 8136a5cb (#11450 (closed)). To fix it, you have to do a tiresome song and dance with auxiliary type families:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Mediabus 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) pt = SSDTicks pt

type family SSDTicks (pt :: StaticTicks) :: StaticTicks where
  SSDTicks (t' :/ r') = t' :/ r'

But after Simon's motivation for this change in #11450 (closed)##13398 (closed), I'm still not convinced that the original program should be rejected. After all, this change was introduced so that associated type families with //multiple// would be rejected. But in the SetStaticDuration example above, there's only one equation, and it's a complete pattern match! So I'm failing to see why it should be rejected.

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	simonpj
Operating system
Architecture

mentioned in issue #13393 (closed)

changed milestone to %8.2.1

changed weight to 7

added Tbug Trac import labels

Upon further thought, I'm not even sure why this particular restriction was added in the first place. #11450 (closed) was about making the type variables used in a class instance head the same as the variables used in the same positions in the associated type family instances. This business about not allowing multiple associated type family instances feels completely orthogonal to that issue (indeed, I wasn't even aware of its existence until just now, as it seems to have been snuck in without a mention in the GHC 8.2 release notes).

Moreover, this additional check is causing code in the wild to fail, and for reasons that I don't comprehend. Simon, what exactly is the problem with allowing code like what is shown in the original program?

Why did you not write (in the original)

instance HasStaticDuration (t :/ r) where
  type SetStaticDuration (t :/ r) pt = pt

I suppose you'll say that since StaticTicks has only one data constructor, replacing pt by (t' :/ r') makes no difference. But what about

type family F a :: StaticTicks

Now I suppose that SetStaticDuration (t :/ r) (F Int) will fail to reduce?

Suppose StaticTicks had a second data constructor Foo. Would you still say that the instance should be accepted?

I was just trying to enforce that the definition was complete, nothing deeper. There is nothing fundamentally wrong with a partial function I suppose.

But really, what's wrong with just using a variable here?

Replying to [ticket:13398#comment:133224 simonpj]:

Why did you not write (in the original) ...

Because I didn't write this code. It's from Hackage.

But really, what's wrong with just using a variable here?

Because that trick will only work in very limited circumstances. To better illustrate the point I'm trying to make, imagine you instead had this code:

instance HasStaticDuration (t :/ r) where
  type SetStaticDuration (t :/r) (t' :/ r') = r' :/ t'

This is a perfectly legitimate associated type family instance (assuming we redefine StaticTicks to have the right type), and moreover, it //requires// pattern-matching on the second argument to SetStaticDuration to define. Yet in GHC HEAD, you cannot do this—you necessarily must jump through hoops to accomplish the same thing.

To better illustrate the point I'm trying to make, imagine you instead had this code:

Ah. Excellent point.

An easy thing to do is simply to lift the check altogether. So the result would be

• The args corresponding to the class parameters must be identical
• The other args can be anything at all

So we'd allow

class C a where
  type F a b
  ...

instance C Int where
  type F Int Bool = Char
  ...

That says nothing about what F Int Char might be; and you can only give instances for F inside a class instance, so you can't extend it later.

We could get this simply by omitting the two check_poly_arg lines in TcValidity.checkConsistntFamInst:

       -- 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)

Alternatively I suppose we could instead elaborate the check to allow single-constructor data types to be pattern matched as above. (Nestedly, I guess.)

Alternatively, we could just make a refutable pattern into a warning. But watch out for type F Int r r, which demands equality.

I don't know which is best. Whatever the outcome, would you like to push this through, Ryan?

I think your first proposal (simply omitting those two checks) would be ideal. I've implemented that in D3302.

Trac metadata

Trac field	Value
Differential revisions	- → D3302

mentioned in commit 67345ccf

Trac metadata

Trac field	Value
Test case	- → indexed-types/should_compile/T13398a, indexed-types/should_compile/T13398b

added 1 deleted label

closed

Merged to ghc-8.2 as 82366c4c.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added Phigh label

mentioned in issue #8161 (closed)