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

[GHC]

#15905: Data familes should end in Type
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14645            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Some thoughts from this morning's call:

 * The error report in the original report is unrelated to this ticket:
 it's just #12088 again. Adding a TH splice does the trick, giving this
 minimal example:

 {{{#!hs
 {-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TemplateHaskell #-}

 module Bug where

 import Data.Kind

 data family Fix (f :: Type -> k) :: k

 type family F a
 type instance F Int = Type -> Type

 $(return [])

 data instance Fix (f :: Type -> F Int) (x :: Type) = Mk
 }}}

     This is accepted, by transforming the instance to

 {{{#!hs
 data instance Fix @(Type -> Type) (f :: Type -> Type) (x :: Type) = Mk
 }}}

     In other words, GHC just realizes it can replace `F Int` with `Type ->
 Type` and carry on.

 * In an attempt to stop GHC from being this clever, we tried using visible
 dependent quantification:

 {{{#!hs
 data family Fix k (f :: Type -> k) :: k
 data instance Fix (F Int) (f :: Type -> F Int) (x :: Type) = Mk
 }}}

     Note that `k` is explicit now. This panics, because the
 `unravelFamInstPats` chokes on the strange instance, causing downstream
 chaos. (Really, `unravelFamInstPats` should panic.) However, if somehow
 the plumbing were fixed, this would be rejected because it mentions a type
 family in a type pattern.

 * In another attempt to defeat the ever-clever GHC, I tried using an
 explicit forall.

 {{{#!hs
 data family Fix (f :: Type -> k) :: k
 data instance forall (f :: Type -> F Int) (x :: Type). Fix f x = Mk
 }}}

 This works by instantiating `Fix` with `Type -> Type` (as before) and
 casting `f`.

 * Previously, Simon was worried about the fact that there might be a
 difference in behavior between eager unification and the work the solver
 does. But I don't think there is, as `solveEqualities` is called
 ''before'' `unravelFamInstPats`.

 * The problem here is really all about when type families get in the way
 of exposing arrows in the data family's kind. In the `Fix` example, the
 type family `F Int` obscures the underlying type `Type -> Type`. How do we
 specify when such a problem exists?

 * I conjecture that the problem never exists on its own. This obfuscation
 can happen only in two ways: (1) either some kind parameter has been
 instantiated with a type family application, or (2) a type family
 application appears in the return kind of a data family. In case (1),
 we're blocked by #12564; that case cannot happen. In case (2), we're
 blocked by #14645. So I think that this ticket, by itself, is redundant
 currently. If either of those other tickets is fixed, it won't be.

 * Fixing #12564 is likely to require generalizing (or otherwise changing)
 the form of type family LHSs, thus fixing this ticket inter alia.

 So, the upshot is: let's fix #12564 before #14645, and this ticket never
 needs to be considered again. :)

 I'm commenting on those two tickets, too.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15905#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler