Opened 3 years ago

Closed 3 years ago

#13398 closed bug (fixed)

Associated type family instance validity checking is too conservative

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: TypeFamilies Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T13398a, indexed-types/should_compile/T13398b
Blocked By: Blocking:
Related Tickets: #11450 Differential Rev(s): Phab:D3302
Wiki Page:

Description

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 8136a5cbfcd24647f897a2fae9fcbda0b1624035 (#11450). 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 https://ghc.haskell.org/trac/ghc/ticket/11450#comment:24, 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.

Change History (9)

comment:1 Changed 3 years ago by RyanGlScott

Upon further thought, I'm not even sure why this particular restriction was added in the first place. #11450 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?

comment:2 Changed 3 years ago by simonpj

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?

comment:3 in reply to:  2 Changed 3 years ago by RyanGlScott

Replying to 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.

Last edited 3 years ago by RyanGlScott (previous) (diff)

comment:4 Changed 3 years ago by simonpj

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?

comment:5 Changed 3 years ago by simonpj

Keywords: TypeFamilies added

comment:6 Changed 3 years ago by RyanGlScott

Differential Rev(s): Phab:D3302
Status: newpatch

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

comment:7 Changed 3 years ago by Ryan Scott <ryan.gl.scott@…>

In 67345cc/ghc:

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

comment:8 Changed 3 years ago by RyanGlScott

Status: patchmerge
Test Case: indexed-types/should_compile/T13398a, indexed-types/should_compile/T13398b

comment:9 Changed 3 years ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.