[Haskell-cafe] Exponential complexity of type checking (Was: Type-level naturals & multiplication)

[Dan Doel]

On Wednesday 14 October 2009 6:15:11 am Roel van Dijk wrote:
> If you declare a type for f5 then ghci must check if that type is
> correct, which triggers the explosion. If you don't declare a type
> then it won't infer the type until necessary. Basically, ghci is lazy

Well, that may be the explanation, but it's a bit more convoluted than I'd 
have initially thought. For instance, if I write:

  e = head ()

it fails immediately with a type error, so clearly it must be doing some level 
of checking immediately. However, it only needs to check 'head' and '()' to 
notice that they're incompatible, so I suppose it may not need to compute the 
type of e (were it well-typed). But then, adding:

  f6 = f5 . f5

produces no more delay than before. Nor does:

  g = snd . f5

So ghci is able to verify that f5 can be instantiated to the forms a -> b and 
b -> c in the first case, and that it is of the form a -> (b,c) in the second 
case, without blowing up. However, either of:

  e     = f5 ()
  e' () = f5 ()

does blow up, so it must be verifying more than the fact that f5 is of the 
form a -> b, where a can be instantiated to (), which is odd if it's smart 
enough to only compute the portion of the type necessary to verify that 
applications can be well typed.

-- Dan