[GHC] #15905: Data familes should end in Type

16 Nov 2018

      #15905: Data familes should end in Type
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Currently we allow
 {{{
 data family Fix (f :: Type -> k) :: k
 }}}
 with a ‘k’ in the right-hand corner. See `Note [Arity of data families]`
 in `FamInstEnv`.

 That seems attractive because we can then have
 {{{
 data instance Fix (f :: Type -> Type -> Type) (x :: Type) = MkFix2 (f (Fix
 f x) x)
 }}}
 But what about this?
 {{{
 type family F a
 type instance F Int = Type -> Type
 data instance Fix (f :: Type -> F Int) (x :: Type) = …
 }}}
 The type inference engine (tcInferApps) will type the LHS as something
 like
 {{{
         ((Fix (f :: Type -> F Int))  |>  co1)
           (x |> co2)

 where  co1 :: F Int ~ Type
        co2 :: Type ~ F Int
 }}}
 But the LHS of a family axiom has to look like
 {{{
         F t1 t2 … tn
 }}}
 not
 {{{
         ((F t1 |> co) t2 t3) |> co4) …tn
 }}}
 with casts in the way.  So that LHS must be rejected.  And it’s very hard
 to see how to accept the first example while (predictably, comprehensibly)
 rejecting the second.  It’d be something like “the kind that instantiates
 k must have obvious, visible, arrows”.  Ugh!

 And indeed GHC HEAD does accept the first, but rejects the second with the
 error message
 {{{
     • Expected kind ‘* -> * -> *’,
         but ‘f :: Type -> F Int’ has kind ‘* -> F Int’
     • In the first argument of ‘Fix’, namely ‘(f :: Type -> F Int)’
       In the data instance declaration for ‘Fix’
 }}}
 That's clearly bogus: we've specified that `F Int = Type -> Type`.  I'm
 not even sure precisely
 how it happens, but it must be fragile: a change in solve order, or more
 aggressive solving
 might change the behaviour.

 I don't see how to solve this.  I propose instead to require data family
 kinds to
 end in `Type`, not in a type ''variable'' (as we currently allow).

 I don't know how many people that would affect, but the current state of
 affairs
 looks untenable.

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