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

[GHC]

#12564: Type family in type pattern kind
-------------------------------------+-------------------------------------
           Reporter:  int-index      |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I want to write a type family that is analogous to `!!` for lists but
 requires the index to be no bigger than the length of the list. Usually,
 in dependently typed languages finite sets are used for this purpose,
 here's an attempt to do so in Haskell:

 {{{#!haskell
 {-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}

 import Data.Kind

 data N = Z | S N

 type family Len (xs :: [a]) :: N where
   Len '[] = Z
   Len (_ ': xs) = S (Len 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 (x ': _) FZ = x
   At (_ ': xs) (FS i) = At xs i
 }}}

 It fails to compile with this error:

 {{{
 FinAt.hs:16:3: error:
     • Illegal type synonym family application in instance: 'FZ
     • In the equations for closed type family ‘At’
       In the type family declaration for ‘At’
 }}}

 That's because the kind of the `FZ` pattern (first clause of `At`) has the
 kind `Fin (Len xs)` and the application of `Len` cannot reduce completely.
 `checkValidTypePat` then disallows the pattern, as it contains a type
 family application.

 I tried to suppress `checkValidTypePat` and the definition of `At` has
 compiled; however, it's of little use, since `At` doesn't reduce:

 {{{#!haskell
 x :: At '[Bool] FZ
 x = True
 }}}

 results in

 {{{
 FinAt.hs:20:5: error:
     • Couldn't match expected type ‘At
                                       * ((':) * Bool ('[] *)) ('FZ 'Z)’
                   with actual type ‘Bool’
     • In the expression: True
       In an equation for ‘x’: x = True
 }}}

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