The Polymorphic Recursion page on Wikipedia gives the following example, where a Haskell type checker cannot infer a type without explicit type annotation:
data Nested a = a :<: (Nested [a]) | Epsilon
length Epsilon = 0
length (_ :<: xs) = 1 + length xs
When compiling this code, GHC says:
Occurs check: cannot construct the infinite type: t ~ [t]
Expected type: Nested t
Actual type: Nested [t]
Relevant bindings include
xs :: Nested [t]
length :: Nested t -> a
I understand how tit becomes [t], but I do not understand why this is a problem for typechecker. If we let lengthbe Nested t -> a, and then stumbled upon length xsand let it be Nested [t] -> b, why can't we assume that a ~ btypecheck it successfully? Or is the problem elsewhere?
source
share