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