Bottom dictionaries can be derived with QuantifiedConstraints, UndecidableInstances and UndecidableSuperClasses
[I'm not sure if this is a bug or documentation issue. I'd prefer the former so I applied "bug" template]
Summary
With QuantifiedConstraints
, UndecidableInstances
and UndecidableSuperClasses
it is possible to
produce bottom dictionary, which isn't mentioned in docs as far as I can see.
Steps to reproduce
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, ConstraintKinds, FlexibleInstances,
GADTs, QuantifiedConstraints, TypeApplications, ScopedTypeVariables #-}
module QCLoop where
class c => Hold c
instance c => Hold c
data Dict c = c => Dict
anythingDict :: Dict c
anythingDict = go
where
go :: (Hold c => c) => Dict c
go = Dict
Produces bottom dictionary
Rec {
$dHold_rxi :: forall {c :: Constraint}. Hold c
$dHold_rxi = $dHold_rxi
end Rec }
anythingDict :: forall (c :: Constraint). Dict c
anythingDict = \ (@c) -> Dict ($dHold_rxi `cast` <Co:2>)
Expected behavior
Either the program is rejected with "could not deduce c" or "too many iterations", or documentation for
UndecidableInstances
and/or UndecidableSuperClasses
mentions that they may result in
non-termination not only in typechecker but also at runtime.
I would really prefer the former as the ability to "prove" anything with such code scares me a bit.
Environment
- GHC version used: 8.10.4, 9.0.1 and 9.1.20210409
- Operating System: Linux (NixOS)
- System Architecture: x86-64