Skip to content

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
Edited by aadaa-fgtaa
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information