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

[Dan Doel]

On Wednesday 14 October 2009 5:25:10 am Roel van Dijk wrote:
> With newtypes I can probably abstract even more. (newtype X a b = X (a (a
>  b))

In fact, with GHC extensions, you don't need newtypes:

  {-# LANGUAGE LiberalTypeSynonyms #-}

  type T a   = (a,a)
  type X f a = f (f a)

  f0 :: a -> T a
  f0 x = (x,x)

  f1 :: a -> X T a
  f1   = f0 . f0

  f2 :: a -> X (X T) a
  f2   = f1 . f1

  f3 :: a -> X (X (X T)) a
  f3   = f2 . f2

  f4 :: a -> X (X (X (X T))) a
  f4   = f3 . f3

> Inferring the type of f5 also stops my machine in its tracks. But I
> *was* able to infer the type of (f4 . f4).
> 
> :t (f4 . f4)
> 
> (f4 . f4) :: a -> T16 (T16 a)
> 
> :t f5

Yeah. Asking for the type of 'f4 . f4' doesn't seem to expand the synonyms, 
while checking f5 does for some reason. I'm perplexed that having f5 defined 
in the file doesn't trigger the explosion unless you declare a type (even in 
terms of X and T) or ask for its type at the prompt.

-- Dan