Mergulhando meu dedo do pé nas águas de tipos dependentes, tive uma rachadura no exemplo canônico da "lista com comprimento estaticamente tipificado".

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

-- a kind declaration
data Nat = Z | S Nat

data SafeList :: (Nat -> * -> *) where
    Nil :: SafeList Z a
    Cons :: a -> SafeList n a -> SafeList (S n) a

-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x

Isso parece funcionar:

ghci> :t Cons 5 (Cons 3 Nil)
Cons 5 (Cons 3 Nil) :: Num a => SafeList ('S ('S 'Z)) a

ghci> safeHead (Cons 'x' (Cons 'c' Nil))
'x'

ghci> safeHead Nil
Couldn't match type 'Z with 'S n0
Expected type: SafeList ('S n0) a0
  Actual type: SafeList 'Z a0
In the first argument of `safeHead', namely `Nil'
In the expression: safeHead Nil
In an equation for `it': it = safeHead Nil

No entanto, para que esse tipo de dados seja realmente útil, eu devo construí-lo a partir de dados em tempo de execução para os quais você não sabe a duração no tempo de compilação. Minha tentativa ingênua:

fromList :: [a] -> SafeList n a
fromList = foldr Cons Nil

Isso falha na compilação, com o erro de tipo:

Couldn't match type 'Z with 'S n
Expected type: a -> SafeList n a -> SafeList n a
  Actual type: a -> SafeList n a -> SafeList ('S n) a
In the first argument of `foldr', namely `Cons'
In the expression: foldr Cons Nil
In an equation for `fromList': fromList = foldr Cons Nil

Entendo por que isso está acontecendo: o tipo de retorno deCons é diferente para cada iteração da dobra - esse é o ponto! Mas não vejo uma maneira de contornar isso, provavelmente porque ainda não li o suficiente sobre o assunto. (Não consigo imaginar todo esse esforço sendo colocado em um sistema de tipos que é impossível de usar na prática!)

Então: como posso construir esse tipo de dados digitados de forma dependente a partir de dados digitados "normais"?

Seguindo o conselho de @ luqui, pude fazerfromList compilar:

data ASafeList a where
    ASafeList :: SafeList n a -> ASafeList a

fromList :: [a] -> ASafeList a
fromList = foldr f (ASafeList Nil)
    where f x (ASafeList xs) = ASafeList (Cons x xs)

Aqui está minha tentativa de descompactar oASafeList e use-o:

getSafeHead :: [a] -> a
getSafeHead xs = case fromList xs of ASafeList ys -> safeHead ys

Isso causa outro erro de tipo:

Couldn't match type `n' with 'S n0
  `n' is a rigid type variable bound by
      a pattern with constructor
        ASafeList :: forall a (n :: Nat). SafeList n a -> ASafeList a,
      in a case alternative
      at SafeList.hs:33:22
Expected type: SafeList ('S n0) a
  Actual type: SafeList n a
In the first argument of `safeHead', namely `ys'
In the expression: safeHead ys
In a case alternative: ASafeList ys -> safeHead ys

Novamente, intuitivamente, faz sentido que isso falhe na compilação. eu posso ligarfromList com uma lista vazia, então o compilador não tem garantia de que poderei chamarsafeHead no resultadoSafeList. Essa falta de conhecimento é aproximadamente o que a existênciaASafeList capturas.

Esse problema pode ser resolvido? Sinto como se tivesse percorrido um beco sem saída lógico.