Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Question

Suppose a Haskell library designer decides to use UndecidableInstances for some reason. The library compiles fine. Now suppose some program uses the library (like defines some instances of its type classes), but doesn't use the extension. Can it happen that the compilation fails (doesn't terminate)?

If such a scenario can happen, I'd be happy to see an example. For example, as mtl uses UndecidableInstances a lot, is it possible to write a program that depends on mtl (or any other standard library that uses the extension), doesn't use UndecidableInstances itself, but fails to compile because of undecidability?

Lanneret

Answer 1

Great question!

In general this is certainly possible. Consider this module:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}

module M where

class C a b | a -> b where
  f :: a -> b

instance C a b => C [a] [b]
  where f = map f

It compiles by itself just fine. However, if you import this module and define

g x = x + f [x]

you'll get

Context reduction stack overflow; size = 201
Use -fcontext-stack=N to increase stack size to N
  C [b] b
In the second argument of `(+)', namely `f [x]'
In the expression: x + f [x]
In an equation for `g': g x = x + f [x]

---

Regarding the mtl instances, I don't see how something like this is possible, but I also don't have a proof that it's not.

Heaps

I was playing with your solution and I managed to cut it down to class C a where f :: a -> a and instance C [[a]] => C [a] where f = id, which doesn't need any other extension but UndecidableInstances. – Lanneret

After examining it mtl, I believe it's not possible to cause the compiler to loop by using it. The only reason it needs the extension is because some of its instances fail the Coverage Condition. But the idea behind the condition is satisfied - all rhs type variables can be inferred from mtl's instance declarations. – Lanneret

Huh, I'm surprised C [[a]] doesn't require FlexibleContexts. – Leanto

It does, but it seems that UndecidableInstances implies FlexibleContexts. – Heaps