Opened 3 weeks ago

Last modified 2 weeks ago

#13909 new bug

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
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:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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 8.2.0.20170623: http://www.haskell.org/ghc/  :? 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 (2)

comment:1 Changed 2 weeks 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 weeks 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
Note: See TracTickets for help on using tickets.