Skip to content

:kind fails with certain QuantifiedConstraints since 8.8

Description and Steps to reproduce

in GHCi:

:set -XQuantifiedConstraints -XExplicitForAll -XConstraintKinds -XUndecidableInstances -XAllowAmbiguousTypes -XNoStarIsType

-- This works:
() :: forall a b . (a => b ~ b) => ()

-- This fails
-- Illegal type synonym family application ‘GHC.Types.Any @Type’ in instance:
-- (b :: GHC.Types.Any @Type) ~ (b :: GHC.Types.Any @Type)
:kind forall a b . (a => b ~ b) => ()

-- Slight changes make it work, these are all okay:
:kind forall a b . (a => b ~ b) => b
:kind forall a b . (a => b ~ a) => ()
:kind forall a b . (b => b ~ b) => ()

This works in 8.6.5.

The reason -XNoStarIsType is here is because otherwise the error message confusingly contains @*, which wouldn't be parsed as visible kind application (correctly it would have to be @(*)).

Expected behavior

I expect :kind forall a b . (a => b ~ b) => () to return Type, as it does in 8.6.5.

Environment

  • GHC version used:

HEAD (8.9.0.20191012)

Edited by Jakob Brünker
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information