Skip to content

Weird interaction between QuantifiedConstraints and TypeFamilies

Summary

The title is kind of bad. The gist of the issue is that deducing Constr X from forall a. Constr a doesn't work if Constr is a result of a type family evaluation.

Steps to reproduce

Here's an example

data Dict c where
    Dict :: c => Dict c

class Class (a :: Type)

type family Class' where
    Class' = Class

test :: (forall a. Class' a) => Dict (Class' Int)
test = Dict

Expected behavior

Since test does typecheck if I replace Class' with Class, I expected it to typecheck the way it's written as well. Instead I get

Could not deduce (Class Int) arising from a use of Dict from the context: 
    forall a. Class' a
bound by the type signature for:
    test :: (forall a. Class' a) => Dict (Class' Int)

Environment

  • GHC version used: 8.6.4

Optional:

  • Operating System: Windows
  • System Architecture: x64
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information