Type family in type pattern kind

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:

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

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

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire, int-index
Operating system
Architecture