dodanie sygnatury typu wywnioskowanego ghci powoduje błąd

Question

Edycja: oto naprawdę prosty przykład. Motywacja do tego przykładu poniżej.

To kompiluje:

{-# LANGUAGE TypeFamilies #-} 

type family F a b 

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

f' [a] = f a 

I ghci informuje, że:

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

Ale jeśli dodamy do tego podpisu wpisz do pliku powyżej, narzeka:

*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. 

Co daje ?

---

Motywacja:

Po obejrzeniu this question, pomyślałem, że być smart-Alec i napisać trochę rozwiązanie żart. Plan ataku powinien zaczynać się od liczb na poziomie typu (jak zwykle), a następnie napisać niewielką funkcję poziomu Args n a c, która daje typ funkcji, który przyjmuje n kopii a i daje c. Następnie możemy napisać małą klasę typów dla różnych n i być na naszej drodze. Oto co Chcę napisać:

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

Byłem zaskoczony, aby dowiedzieć się, że to nie typ sprawdzić!

Answer 1

Jest to błąd GHC, jak można wykazać za pomocą następujących, jeszcze bardziej uproszczony przykład:

type family F a 

f :: b -> F a 
f = undefined 

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

Proponuję zgłoszenie go do GHC HQ.