#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