aggiungendo la firma del tipo inferito di ghci causa un errore

Question

Modifica: Ecco un esempio davvero semplice. Motivazione per questo esempio qui sotto.

Questo compila:

{-# LANGUAGE TypeFamilies #-} 

type family F a b 

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

f' [a] = f a 

E ghci riporta che:

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

Ma se aggiungiamo questa firma tipo per il file di cui sopra, si lamenta:

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

ciò che dà ?

---

Motivazione:

Dopo aver visto this question, ho pensato che sarei una smart-alec e scrivere un po 'di soluzione di battuta. Il piano di attacco è quello di iniziare con i numeri a livello di codice (come al solito), quindi scrivere una piccola funzione a livello di tipo Args n a c che restituisce il tipo di funzione che prende n copie di a e produce uno c. Quindi possiamo scrivere un po 'di classe per i vari n ed essere sulla buona strada. Ecco quello che voglio a scrivere:

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

Sono stato sorpreso di scoprire che questo non digitare-check!

Answer 1

Questo è un bug GHC, come può essere dimostrato dal seguente, ulteriormente semplificata esempio:

type family F a 

f :: b -> F a 
f = undefined 

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

Suggerisco segnalarlo alla GHC HQ.