Opened 2 years ago

Closed 2 years ago

#13909 closed bug (fixed)

Misleading error message when partially applying a data type with a visible quantifier in its kind

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T13909
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:

{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data Hm (k :: Type) (a :: k) :: Type

class HasName (a :: k) where
  getName :: proxy a -> String

instance HasName Hm where
  getName _ = "Hm"

This is rejected, however:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:11:18: error:
    • Expecting two more arguments to ‘Hm’
      Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
    • In the first argument of ‘HasName’, namely ‘Hm’
      In the instance declaration for ‘HasName Hm’
11 | instance HasName Hm where
   |                  ^^

The culprit appears to be the fact that Hm has kind forall k -> k -> *, which uses a visible quantifier. Does this prevent partial applications of Hm? Or is this simply a GHC bug?

Change History (4)

comment:1 Changed 2 years ago by goldfire

Other than the "expecting two more arguments" part (it should be "one", not "two"), this is correct behavior. What you're trying to do would require impredicative polymorphism in kinds, as you want the kind variable k to expand to a type involving a forall.

We can keep this open as an example of a misphrased error message, but rejection is the correct action until we have impredicativity.

comment:2 Changed 2 years ago by RyanGlScott

Summary: Can't partially apply a data type with a visible quantifier in its kindMisleading error message when partially applying a data type with a visible quantifier in its kind

comment:3 Changed 2 years ago by Ben Gamari <ben@…>

In 89c8d4d2/ghc:

Fix #13909 by tweaking an error message.

GHC was complaining about numbers of arguments when the real
problem is impredicativity.

test case: typecheck/should_fail/T13909

comment:4 Changed 2 years ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T13909

As noted above, we can't really "fix" this any further without implementing support for impredicative types, so I consider this ticket to be resolved.

Note: See TracTickets for help on using tickets.