ghci'nin sonlandırılmış tür imgesini eklemek için bir hata neden olur

Question

Düzenleme: İşte gerçekten basit bir örnek. Aşağıdaki bu örnek için motivasyon.

{-# LANGUAGE TypeFamilies #-} 

type family F a b 

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

f' [a] = f a 

Ve GHCi bildirir:

Bu derler Yukarıda dosyaya bu tür imza eklemek Ama eğer şikayet

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

:

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

Ne verir ?

---

Motivasyon:

this question gördükten sonra ben bir akıllı Alec olmak ve biraz şaka çözümü yazmak düşündüm. Saldırı planı, (her zamanki gibi) tip düzeyindeki sayılarla başlayıp, Args n a c tipini yazıp a kopyasını alan ve c değerini veren işlev türünü yazacaktır. Sonra çeşitli n için biraz tip sınıf yazabilir ve yolumuza devam edebiliriz. İşte yazmak istiyorum ne:

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

Bu tip kontrol bulunmadığı ortaya şaşırdı!

Answer 1

aşağıdaki hususlar ile ispat edilebilir gibi bu bir GHC hata, daha da basitleştirilmiş bir örnek: Ben GHC HQ Bildirmeden öneririz

type family F a 

f :: b -> F a 
f = undefined 

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

.