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

8 Feb 2019

      #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):

 For anyone reading this ticket who is searching for a workaround:

 While I haven't found a general-purpose way to avoid this bug, in limited
 situations it's often possible to rewrite your type families in a way that
 shifts applications of type families from the left-hand side to the right-
 hand side. For example, GHC //does// accept this formulation of `At`:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}

 import Data.Kind
 import Data.Type.Equality

 data N = Z | S N

 type family Len (xs :: [a]) :: N where
   Len '[] = Z
   Len (_ ': xs) = S (Len xs)

 data Vec :: N -> Type -> Type where
   VNil :: Vec Z a
   (:>) :: a -> Vec n a -> Vec (S n) a

 type family ListToVec (l :: [a]) :: Vec (Len l) a where
   ListToVec '[]    = VNil
   ListToVec (x:xs) = x :> ListToVec xs

 data Fin :: N -> Type where
   FZ :: Fin (S n)
   FS :: Fin n -> Fin (S n)

 type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
   At xs i = At' (ListToVec xs) i

 type family At' (xs :: Vec n a) (i :: Fin n) :: a where
   At' (x :> _)  FZ     = x
   At' (_ :> xs) (FS i) = At' xs i

 -- Unit tests
 test1 :: At '[True] FZ :~: True
 test1 = Refl

 test2 :: At [True, False] FZ :~: True
 test2 = Refl

 test3 :: At [True, False] (FS FZ) :~: False
 test3 = Refl
 }}}

 If you inspect the definition of `At`, you'll see why this works:

 {{{
 λ> :info At
 type family At @a (xs :: [a]) (i :: Fin (Len @a xs)) :: a where
   forall a (xs :: [a]) (i :: Fin (Len @a xs)).
     At @a xs i = At' @(Len @a xs) @a (ListToVec @a xs) i
 }}}

 Note that the left-hand side, `At @a xs i`, does not contain any immediate
 uses of `Len`. (The kind of `i` does, but thankfully, GHC doesn't consider
 that to be an illegal type synonym family application.) The other uses of
 `Len` and `ListToVec` have been quarantined off on the right-hand side,
 where GHC can't complain about them.

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