Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?

like image 725
Petr Avatar asked Jan 23 '13 09:01

Petr


1 Answers

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.

like image 94
Roman Cheplyaka Avatar answered Oct 16 '22 05:10

Roman Cheplyaka