Почему GHC не может вывести этот тип?

Question

Рассмотрим следующий фрагмент кода (от 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 выдает следующее сообщение об ошибке:

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 

Почему нельзя GHCI вывести тип?

Или, в следующем коде, pure 'и компиляция good_f, в то время как bad_f дает аналогичное сообщение об ошибке. Зачем?

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

Как было предложено пользователем2407038, включение -XMonoLocalBinds заставляет код работать.