[GHC] #13398: Associated type family instance validity checking is too conservative

8 Mar 2017

      #13398: Associated type family instance validity checking is too conservative
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #11450
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 `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:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler