UndecidableSuperClasses fails to terminate when inferring type in where-clause
Summary
When defining a class with a recursive constraint on an associated type family, functions using that constraint fail to type check when inferring type in a where clause.
Related to:
Steps to reproduce
The following fails on all GHC versions I've tested, 8.2 to 9.4.1-rc1.
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableSuperClasses #-}
import Data.Kind
class (Monad m, MyMonad (Inner m)) => MyMonad m where
type Inner m :: Type -> Type
foo :: m Int
works :: MyMonad m => m String
works = show <$> ((+ 1) <$> foo)
fails :: MyMonad m => m String
fails = show <$> fooPlusOne
where
fooPlusOne = (+ 1) <$> foo
alsoFails :: MyMonad m => m String
alsoFails =
let fooPlusOne = (+ 1) <$> foo
in show <$> fooPlusOne
This errors with:
• solveWanteds: too many iterations (limit = 4)
Unsolved: WC {wc_simple =
[D] _ {0}:: Monad f0 (CDictCan)
[D] _ {0}:: Monad (Inner f0) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Monad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: Applicative f0 (CDictCan)
[D] _ {0}:: Applicative (Inner f0) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Applicative (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dFunctor_aJ3 {0}:: Functor f0 (CDictCan)
[D] _ {0}:: Functor (Inner f0) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: Functor (Inner (Inner (Inner f0))) (CDictCan)
[WD] $dMyMonad_aJM {0}:: MyMonad f0 (CDictCan)
[D] _ {0}:: MyMonad (Inner f0) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner f0)) (CDictCan)
[D] _ {0}:: MyMonad (Inner (Inner (Inner f0))) (CDictCan)
[D] _ {0}:: MyMonad
(Inner (Inner (Inner (Inner f0)))) (CDictCan(psc))}
Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
At least GHC 9.4.1-rc1 gives a slightly better error message in addition to too many iterations
:
• Could not deduce (Monad
(Inner (Inner (Inner (Inner (Inner m))))))
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner (Inner m)))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner (Inner m))))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner (Inner m)))’,
arising from a superclass required to satisfy ‘MyMonad
(Inner (Inner m))’,
arising from a superclass required to satisfy ‘MyMonad (Inner m)’,
arising from a superclass required to satisfy ‘MyMonad m’,
arising from a use of ‘foo’
Expected behavior
I know -XUndecidableSuperClasses
always carries a risk of non-termination. Is this one of those cases that's known to just not work? Or should we try to make this work?
At the very least, I don't see any other issues around this simple example of just moving a thing into a where clause, so this at least provides a locus for discussion. It's also workaround-able by explicitly typing the helper function.
Environment
- GHC version used: tested all GHC versions from 8.2 to 9.4.1-rc1
Optional:
- Operating System:
- System Architecture: