29

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?

Petr
  • 62,528
  • 13
  • 153
  • 317

1 Answers1

22

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.

Roman Cheplyaka
  • 37,738
  • 7
  • 72
  • 121
  • 5
    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`. – Petr Jan 23 '13 at 20:38
  • 4
    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](http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/type-class-extensions.html#instance-rules). But the idea behind the condition is satisfied - all rhs type variables can be inferred from `mtl`'s instance declarations. – Petr Jan 23 '13 at 20:39
  • Huh, I'm surprised `C [[a]]` doesn't require `FlexibleContexts`. – Ben Millwood Feb 02 '13 at 21:01
  • 4
    It does, but it seems that `UndecidableInstances` implies `FlexibleContexts`. – Roman Cheplyaka Feb 02 '13 at 21:05