Help me figure out why GHC loops in a functional dependencies + undecidable instances scenario.
I am learning functional dependencies. The GHC manual has a section on rules that instance declaration must follow. One in particular (“Coverage Condition”) applies to functional dependencies.
The manual states that you can lift these restrictions with UndecidableInstances, but stresses that it can cause havoc, including the type-checker going into a loop.
A specific example is provided at the end of the paragraph (here slightly abridged):
{-# Language FunctionalDependencies #-}
{-# Language UndecidableInstances #-}
module Prova where
class Mul a b c | a b -> c where
(.*.) :: a -> b -> c
instance Mul Int Int Int where (.*.) = undefined
instance Mul Int Float Float where (.*.) = undefined
instance Mul a b c => Mul a [b] [c] where (.*.) = undefined
f b x y = if b then x .*. [y] else y
And indeed if you load it wit ghci, you get an error:
prova.hs:13:23-25: error:
• Reduction stack overflow; size = 201
When simplifying the following type: Mul a0 [[c]] [c]
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: x .*. [y]
In the expression: if b then x .*. [y] else y
In an equation for ‘f’: f b x y = if b then x .*. [y] else y
|
13 | f b x y = if b then x .*. [y] else y
| ^^^
To understand the example, I decided to work it step by step, to see exactly where the type-checker goes into a loop:
// Type-check this:
// f b x y = if b then x .*. [y] else y
b :: Bool
x :: a
y :: b
// Let's tackle `x .*. [y]`
// The only instance head that matches is `Mul a [b] [c]`.
x :: a
[y] :: [b]
// Constraint: Mul a [b] [c] => …
// And from `else y` we get
y :: [c]
// Then we can say `b ~ [c]`, right? (unification?) So the signature becomes
f :: Mul a [[c]] [c] => Bool -> [c] -> [c]
And indeed if you add f :: Mul a [[c]] [c] => Bool -> a -> [c] -> [c], the code at the top does compile, albeit with this warning:
prova.hs:14:6-47: warning: [-Wsimplifiable-class-constraints]
• The constraint ‘Mul a [[c]] [c]’ matches
instance Mul a b c => Mul a [b] [c] -- Defined at prova.hs:11:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature:
f :: Mul a [[c]] [c] => Bool -> a -> [c] -> [c]
|
14 | f :: Mul a [[c]] [c] => Bool -> a -> [c] -> [c]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Wsimplifiable-class-constraints warns you when you — e.g. — write Eq [a] => a -> a instead of Eq a => a -> a.
In this case simply removing a pair of extra brackets from the type parameters in Mul a [[c]] [c] should do. And indeed with:
f :: Mul a [c] c => Bool -> a -> [c] -> [c]
the example compiles.
If you have read until here, thanks! My question is: why was the type-checker not able to deduce this signature on its own?