[GHC] #12564: Type family in type pattern kind

[GHC]

#12564: Type family in type pattern kind
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |             Keywords:  TypeInType,
      Resolution:                    |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:  14119             |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 The trick from comment:17 can be further generalized to a pseudo-algorithm
 that (I think) would work for any closed type family that suffers from
 this problem. Here is what you have to do:

 1. Identity any "problematic" type families that cause the `Illegal type
 synonym family application in instance` error. In the original example,
 the only problematic type family is `Len`.
 2. Encode each problematic type families as an inductive proposition. In
 the particular case of `Len`, this would look this like:

    {{{#!hs
    data LenProp :: forall a. [a] -> N -> Type where
      LenNil  :: LenProp '[] Z
      LenCons :: LenProp xs n -> LenProp (x:xs) (S n)
    }}}

    The type family's argument kinds (e.g., `[a]`) as well as the return
 kind (e.g., `N`) become part of the proposition's kind. Each constructor
 encodes a single equation of the type family. The `LenNil` constructor
 encodes the `Len '[] = Z` equation, and its return type of `LenProp '[] Z`
 encodes the fact that this equation takes `'[]` as an argument and returns
 `Z`. Similarly, the `LenCons` constructor encodes the `Len (_ ': xs) = S
 (Len xs)` equation, and the field of type `LenProp xs n` encodes the
 recursive call to `Len` on the right-hand side of the equation. Notice
 that we "bind" the result of this recursive call to `n` and use `S n` in
 the return type, since the equation applies `S` to the recursive `Len`
 call.
 3. Take all type families that were rejected previously due to occurrences
 of problematic type families and define "internal" versions of them using
 the newly defined proposition types. In the particular case of `At`, this
 would look this:

    {{{#!hs
    type family At' (xs :: [a]) (lp :: LenProp xs r) (i :: Fin r) :: a
 where
      At' (x:_)  (LenCons _)  FZ     = x
      At' (_:xs) (LenCons lp) (FS i) = At' xs lp i
    }}}

    Note that `Len` does not appear anywhere in this definition. Where we
 previously had `Fin (Len xs)` we now have `Fin r`, where the `r` is bound
 by a new argument of kind `LenProp xs r`. In general, you'll need to
 introduce as many new arguments with proposition kinds as is necessary to
 replace all occurrences of problematic type families.
 4. For each proposition-encoded type family, define another type family
 that translates the arguments of the original type family to the
 corresponding proposition. For example, the following type family
 translates a list to a `LenProp`:

    {{{#!hs
    type family EncodeLenProp (xs :: [a]) :: LenProp xs (Len xs) where
      EncodeLenProp '[]    = LenNil
      EncodeLenProp (_:xs) = LenCons (EncodeLenProp xs)
    }}}

    Note the return kind of `LenProp xs (Len xs)`. This is important, since
 this is how we are going to "sneak in" a use of `Len` into `At` in the
 next step. Note that `Len` is not problematic in `EncodeLenProp` itself
 since `Len` never worms its way into a left-hand-side argument.
 5. Finally, redefine type families in terms of the "internal" ones created
 in step (3). In the particular case of `At`, it would become:

    {{{#!hs
    type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
      At xs i = At' xs (EncodeLenProp xs) i
    }}}

    This uses `EncodeLenProp` to sneak a use of `Len` into `At'`.
 Critically, this definition avoids pattern-matching on `i` (since that
 would trigger the `Illegal type synonym family application in instance`
 error). All that `At` does now is pass its arguments along to `At'`, which
 does the real work on the proposition created by `EncodeLenProp`. In this
 version of `At`, the only place where `Len` occurs on the left-hand side
 is in the kind of `i`, which GHC deems acceptable.

 My program in comment:17 essentially follows the algorithm above, except
 it uses a slightly more complicated type, `Vec`, instead of `LenProp`.

 -----

 This seems to work for all of the closed type families that I've
 encountered that suffer from this issue. That being said, this trick
 doesn't really work well in the setting of //open// type families, as it's
 not always possible to know //a priori// which kind arguments in an open
 type family might end up being instantiated with type families. If you
 figure out a general workaround for that, let me know :)

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