Pourquoi GHC ne peut-il pas en déduire ce type?

Question

Tenir compte de l'extrait de code suivant (de http://lpaste.net/180651):

{-# LANGUAGE ScopedTypeVariables #-} 

class Natural n 

newtype V n a = V [a] 

dim :: Natural n => V n a -> Int 
dim = undefined -- defined in my actual code 

bad_fromList :: Natural n => [a] -> V n a 
bad_fromList l = if length l == dim v then v else undefined -- this is line 11 
    where v = V l 

good_fromList :: forall n a. Natural n => [a] -> V n a 
good_fromList l = if length l == dim v then v else undefined 
    where v = V l :: V n a 

GHCi donne le message d'erreur suivant:

test.hs:11:33: error: 
    • Could not deduce (Natural n0) arising from a use of ‘dim’ 
     from the context: Natural n 
     bound by the type signature for: 
        bad_fromList :: Natural n => [a] -> V n a 
     at test.hs:10:1-41 
     The type variable ‘n0’ is ambiguous 
    • In the second argument of ‘(==)’, namely ‘dim v’ 
     In the expression: length l == dim v 
     In the expression: if length l == dim v then v else undefined 

Pourquoi ne peut GHCi déduire le type? Ou, dans le code suivant, pur 'et good_f compiler, alors que bad_f donne un message d'erreur similaire. Pourquoi?

pure' :: Natural n => a -> V n a 
pure' x = v 
    where v = V $ replicate (dim v) x 

bad_f :: Natural n => [a] -> (V n a, Int) 
bad_f xs = (v, dim v) 
    where v = V xs 

good_f :: Natural n => a -> (V n a, Int) 
good_f x = (v, dim v) 
    where v = V $ replicate (dim v) x 

Answer 1

Comme suggéré par user2407038, l'activation de -XMonoLocalBinds permet au code de fonctionner.