al agregar la firma de tipo inferido de ghci provoca un error

Question

Editar: Aquí hay un ejemplo verdaderamente simple. Motivación para este ejemplo a continuación.

Esto compila:

{-# LANGUAGE TypeFamilies #-} 

type family F a b 

f :: a -> F a b 
f = undefined 

f' [a] = f a 

Y ghci informa que:

*Main> :t f' 
f' :: [a] -> F a b 

Pero si añadimos este tipo de firma en el fichero anteriormente, se queja:

*Main> :r 
[1 of 1] Compiling Main    (test.hs, interpreted) 

test.hs:9:14: 
    Couldn't match type `F a b0' with `F a b' 
    NB: `F' is a type function, and may not be injective 
    In the return type of a call of `f' 
    In the expression: f a 
    In an equation for `f'': f' [a] = f a 
Failed, modules loaded: none. 

lo que da ?

---

motivación:

Después de ver this question, pensé que sería un smart-alec y escribo una solución broma poco. El plan de ataque es comenzar con números de nivel de tipo (como de costumbre), luego escribir una pequeña función de tipo de nivel Args n a c que produce el tipo de función que toma n copias de a y produce un c. Entonces podemos escribir una pequeña clase de tipo para los diversos n y estar en camino. Esto es lo que quiero a escribir:

{-# LANGUAGE TypeFamilies #-} 

data Z = Z 
data S a = S a 

type family Args n a c 
type instance Args Z a c = c 
type instance Args (S n) a c = a -> Args n a c 

class OnAll n where 
    onAll :: n -> (b -> a) -> Args n a c -> Args n b c 

instance OnAll Z where 
    onAll Z f c = c 

instance OnAll n => OnAll (S n) where 
    onAll (S n) f g b = onAll n f (g (f b)) 

Me sorprendió al descubrir que esto no escriba a comprobar!

Answer 1

Esto es un error GHC, como se puede demostrar por el siguiente, aún más simplificada ejemplo:

type family F a 

f :: b -> F a 
f = undefined 

f' :: b -> F a 
f' a = f a 

Sugiero informar a GHC HQ.