# GHC: FunctionalDependencies, UndecidableInstances, and the type-checker

**URL:** <https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761>\
**Category:** Learn\
**Created:** [November 19, 2024, 6:19pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761 "2024-11-19T18:19:55Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![f-a](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/f-a/32/2740_2.png) [@f-a](https://discourse.haskell.org/u/f-a)\
**Post date:** [November 19, 2024, 6:19pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/1 "2024-11-19T18:19:55Z")

</div>

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](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.html#instance-termination-rules) 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):

```haskell
{-# 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:

```haskell
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:

```haskell
// 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:

```haskell
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`](https://downloads.haskell.org/ghc/8.8.4/docs/html/users_guide/using-warnings.html#ghc-flag--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:

```haskell
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?

---

<div class="post-metadata">

**Author:** ![atravers](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@atravers](https://discourse.haskell.org/u/atravers)\
**Post date:** [November 19, 2024, 7:02pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/2 "2024-11-19T19:02:47Z")

</div>

> `Use -freduction-depth=0 to disable this check`

I’ve seen that _“hint”_ before:

> [@Reduction stack overflow](http://discourse.haskell.org/t/reduction-stack-overflow/10193/2):
>
> Some of the articles found during a brief websearch using ghc haskell "reduction stack" increase mention this option: 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) On my system: # ghci -freduction-depth=0 Foo.hs GHCi, version 9.8.2: https://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Foo ( Foo.hs,…

These _could_ be relevant:

> [@Reduction stack overflow](http://discourse.haskell.org/t/reduction-stack-overflow/10193/4):
>
> I think this program indeed yields an infinite loop in the constraint solver. The issue is that MonadWriter e (m e) has Monoid e as a superclass, so when GHC tries to solve the Applicative (m [Foo]) constraint arising from pure: It can use the quantified constraint to get MonadWriter [Foo] (m [Foo]) (and hence Monad (m [Foo]) and hence Applicative (m [Foo])), if only it can solve Monoid [Foo]. Now in order to produce Monoid [Foo], rather than using the global instance, it foolishly decides to …

> [@Reduction stack overflow](http://discourse.haskell.org/t/reduction-stack-overflow/10193/9):
>
> It means you would never be able to use foo, as instantiating it would require a solution to every constraint ever dreamed up by machine or man. A more effective workaround for this specific case would be foo :: (Monoid [Foo], forall e. Monoid e =\> MonadWriter e (m e)) =\> m [Foo] Int foo = pure 1 (You’ll get a compiler warning about a simplifiable class constraint—accurate, but you made me do this, GHC!)

---

<div class="post-metadata">

**Author:** ![simon](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/simon/32/3292_2.png) [@simon](https://discourse.haskell.org/u/simon)\
**Post date:** [November 19, 2024, 9:30pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/3 "2024-11-19T21:30:02Z")

</div>

I think I have an idea why you run this this problem. Let’s revisit `f b x y = if b then x .*. [y] else y`.

```haskell
x :: a
y :: b

```

```haskell
x .*. [y] -- matches Mul a b c => Mul a [b] [c]
x .*. [y] :: [c]

```

Due to the else branch:

```haskell
y :: [c]

```

You still need to resolve `Mul a b c`. Lets fill in `[c]` for `b`: `Mul a b c ~ Mul a [c] c`

This matches again with `Mul a b c => Mul a [b] [c]`. Therefore, from `Mul a [c] c` we can infer `Mul a c d => Mul a [c] [d]` where `c ~ [d]`. We know that `c` must be some kind of list due to the functional dependency. That’s why I have added `c ~ [d]`.

Now, `y` already has the type that it is a list of lists:

```haskell
y :: [[d]]

```

As you match `Mul a b c => Mul a [b] [c]` more and more, the type of `y` grows and grows as more nested list types are inferred. You essentially run into an infinite loop. GHC will cancel type checking after a certain depth.

**Why does `f :: Mul a [c] c => Bool -> a -> [c] -> [c]` typecheck?**  
I have not tested this, but I think what is happening is that you delay the infinite expansion of the typeclass instances. You tell GHC in the signature that `Mul a [c] c` is in scope, therefore GHC will not try to resolve `Mul a [c] c` any further and `f` typechecks.

However, when you try to use `f`, GHC still needs to resolve `Mul a [c] c`. You will once again run into the problem that `Mul a [c] c` results in an infinite recursion of typeclass matchings.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [November 19, 2024, 9:56pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/4 "2024-11-19T21:56:13Z")

</div>

A couple of tips to do with that `Reduction stack overflow` message

> [@atravers](#):
>
> I’ve seen that _“hint”_ before:

Yes. It hardly never helps to drop the check/if your instances genuinely are loopy, the compiler will just take longer to arrive at the same overflow.

GHC’s implementation of FunDeps – errm, leaves a lot to be desired [\*\*\*]. I would write all instances in this form [\*\*]:

```haskell
instance c ~ Int => Mul Int Int c where (.*.) = undefined
instance c ~ Float => Mul Int Float c where (.*.) = undefined
instance (c' ~ [c], Mul a b c) => Mul a [b] c' where (.*.) = undefined

```

Why? Because then instance selection can’t fail due to GHC being unable to figure out whether the result type matches or is at least unifiable with the Wanted. The bare fresh tyvar in the instance head guarantees the right instance is selected; the type improvement (via `~`) is then sure to apply.

I’m not saying this’ll help for your example (it didn’t – see **Answer** below). It’ll at least help split out the steps GHC is going through.

[\*\*] This form is an improvement where you have exactly one FunDep, as in this case. It can make things worse if you have multiple/multi-directional FunDeps, because then it’s not as simple as a single position being the target.

> [@f-a](#):
>
> ```haskell
> f :: Mul a [c] c => Bool -> a -> [c] -> [c]
> 
> ```
> 
> [with that signature] the example compiles.

Hmm merely compiling is not enough. Can you call `f True (1 :: Int) [2, 3 :: Int]` ?

**Answer** No, for example:

```haskell
ff = f True (1::Int) [2, 3::Int]
-- (or merely at the GHC prompt, ask for the `:type` of that call to `f`)

    * Couldn't match type `Int' with `[Int]' arising from a use of `f'
    * In the expression: f True (1 :: Int) [2, 3 :: Int]

```

IOW given that third instance for `Mul`, `f`’s attempt to unify both branches of the `if` is necessarily loopy. By putting that constraint on `f` you’ve merely deferred the check – as @simon says: GHC is being over-generous; perhaps you’re going to import this module into somewhere that has another instance for `Mul` that will break the loop.

> [@f-a](#):
>
> why was the type-checker not able to deduce this signature on its own?

a) Because there’s all sorts of constraints you might put on `f` that would get that code to compile (in particular the compiler isn’t going to guess at what other instances there might be in other modules); but  
b) ‘get to compile’ is not the objective. We want ‘get to be runnable’, and the signature you put doesn’t achieve that.

[\*\*\*] For example, in Hugs:

- Your original code gets rejected with much the same message `type checker has reached the cutoff limit ... may[be] undecidable`.
- Adding the signature you give for `f` _doesn’t_ compile:

> ```haskell
> Inferred type is not general enough
> *** Expected type : Mul a [b] b => Bool -> a -> [b] -> [b] -- from the sig.
> *** Inferred type : Mul a [[b]] [b] => Bool -> a -> [[b]] -> [[b]]
> 
> ```

- This sig (without any call to `f`) does compile – but note it seems to be more general than the `Inferred type` above …

> ```haskell
> f :: Mul a [[c]] [c] => Bool -> a -> [c] -> [c]
> 
> ```

- … except asking for `:type f` takes us back to the `cutoff limit` message.
- And/or trying to define `ff`:

> ```haskell
> Constraints are not consistent with functional dependency
> *** Constraint : Mul Int [Int] Int -- inferred from the else branch result y
> *** And constraint : Mul Int [Int] [a] -- inferred from the then branch/use of (.*.)
> 
> ```

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [November 20, 2024, 1:37am UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/5 "2024-11-20T01:37:46Z")

</div>

> [@f-a](#):
>
> why …

I guess the shortcut answer is: your Wanted type is infinite. Haskell doesn’t support infinite types, so that’s a contradiction. Ex nihilo quodlibet. It’s then down to compiler ergonomics as to what hints it can give/which particular line of code it should point at/whether it could or should suggest any improvement.

---

<div class="post-metadata">

**Author:** ![f-a](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/f-a/32/2740_2.png) [@f-a](https://discourse.haskell.org/u/f-a)\
**Post date:** [November 20, 2024, 2:16pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/6 "2024-11-20T14:16:48Z")

</div>

Thanks everyone for their answer.  
I am still trying to understand this fully, it will take some more tries with manual type-checking.

I will ask for more if needed, for now I am grateful for the explanations!

---

<div class="post-metadata">

**Author:** ![f-a](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/f-a/32/2740_2.png) [@f-a](https://discourse.haskell.org/u/f-a)\
**Post date:** [November 24, 2024, 3:40pm UTC](https://discourse.haskell.org/t/ghc-functionaldependencies-undecidableinstances-and-the-type-checker/10761/7 "2024-11-24T15:40:07Z")

</div>

After reading the original paper from where the example is taken, I have a precise explanation of why this fails. I will write it here if anyone in the future finds this thread via search.

Propedeutic knowledge:

1. The type inference algorithm will try to always infer the most general type. That similarly applies to constraints. Example, if a type of a function is

2. Functional dependencies constraint the value of a parameter in a typeclass.  
When we write `class Multiply a b c | a b -> c where …` we are constraining type `c` based on the value of `a` and `b`.  
Example: with `instance Multiply Int [Int] Int`. and a typeclass function `mul :: a -> b -> c`, `mul 8 [18, 2]` would match and have `c ~ [Int]` (`c` would not have been inferred without the functional dependency).  
This map is called _type improvement_: in this case we don’t want the most general type.

Once you see this two objectives side-to-side, it is immediately clear which problems can arise with type parameters.

Let us copy the code again:

```haskell
{-# 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

```

If you infer the the type of `f` with pencil and paper you will end up with `Mul a [[c]] [c]`.

We now can, checking the instance `instance Mul a b c => Mul a [b] [c]`, remove the extra `[]` and simplify this to `Mul a [c] c`.

Finally the functional dependency `a [b] -> [c]` allows the compiler to improve the type `Mul a [c] c` to `Mul a [[d]] [d]`.

We make a simplifying pass again, and the loop continues.