Sumergiendo mi dedo del pie en las aguas de los tipos dependientes, tuve una grieta en el ejemplo canónico de "lista con longitud estáticamente escrita".

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

Esto 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

Sin embargo, para que este tipo de datos sea realmente útil, debería poder construirlo a partir de datos de tiempo de ejecución para los que no conoce la longitud en el momento de la compilación. Mi ingenuo intento:

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

Esto no se compila, con el error 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

Entiendo por qué sucede esto: el tipo de retorno deCons es diferente para cada iteración del pliegue, ¡ese es el punto! Pero no puedo ver una forma de evitarlo, probablemente porque no he leído lo suficiente sobre el tema. (¡No puedo imaginar que todo este esfuerzo se esté poniendo en un sistema de tipos que es imposible de usar en la práctica!)

Entonces: ¿Cómo puedo construir este tipo de datos de tipo dependiente a partir de datos de tipo "normal"?

Siguiendo el consejo de @ luqui pude hacerfromList 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)

Aquí está mi intento de descomprimir elASafeList y úsalo:

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

Esto causa otro tipo de error:

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

De nuevo, intuitivamente tiene sentido que esto no se pueda compilar. puedo llamarfromList con una lista vacía, por lo que el compilador no tiene garantía de que pueda llamarsafeHead en el resultanteSafeList. Esta falta de conocimiento es aproximadamente lo que existeASafeList capturas

¿Se puede resolver este problema? Siento que podría haber caminado por un callejón sin salida lógico.