Opened 17 months ago

Closed 16 months ago

Last modified 16 months ago

#11635 closed bug (fixed)

Higher-rank kind in datatype definition rejected

Reported by: phadej Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 8.0.1-rc2
Keywords: TypeInType Cc: kosmikus, ocharles
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: dependent/should_compile/T11635
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

Example program:

{-# LANGUAGE TypeInType, KindSignatures, ExplicitForAll #-}
import Data.Kind
data X (a :: forall k. k -> * ) = X

errors with

polykind.hs:3:1: error:
    Expecting one more argument to ‘a’
    Expected kind ‘k0’, but ‘a’ has kind ‘forall k. k -> *’

Without TypeInType, the error is better, yet gives false hint:

polykind.hs:3:23: error:
    Illegal kind: forall k. k -> *
    Did you mean to enable TypeInType?

---

For the record 7.10.3 doesn't recognise polymorphic kinds at all (same program, without Data.Kind import):

polykind.hs:3:23: parse error on input ‘forall’

Which makes me think that polymorphic kinds are somehow supported, but maybe not.

Change History (7)

comment:1 Changed 17 months ago by simonpj

Keywords: TypeInType added

comment:2 Changed 17 months ago by phadej

And I found a workaround to make a code compile. It's not usable, but that's probably another issue:

{-# LANGUAGE TypeInType, ImpredicativeTypes, KindSignatures, ExplicitForAll #-}
import Data.Kind
import Data.Proxy
newtype X (a :: forall k. k -> * ) = X { x :: a Bool -> a (*) }

-- X { x = \_ -> Proxy :: Proxy (*) }
{-
fails with:

    • Couldn't match kind ‘forall k1. k1 -> *’ with ‘forall k. k -> *’
      When matching the kind of ‘Proxy’
    • In the expression: Proxy :: Proxy *
      In the ‘x’ field of a record
      In the expression: X {x = \ _ -> Proxy :: Proxy *}

-}

comment:3 Changed 17 months ago by goldfire

Owner: set to goldfire
Summary: Missleading error message when using polymorpic kindsHigher-rank kind in datatype definition rejected

I think the original program should be accepted. I see nothing wrong with it.

comment:4 Changed 16 months ago by ocharles

Cc: ocharles added

comment:5 Changed 16 months ago by Richard Eisenberg <eir@…>

In 1701255/ghc:

Fix #11635 / #11719.

Instead of creating a new meta-tyvar and then unifying it with
a known kind in a KindedTyVar in a LHsQTyVars, just use the known kind.

Sadly, this still doesn't make #11719 usable, because while you can
now define a higher-kinded type family, you can't write any equations
for it, which is a larger problem.

test cases: dependent/should_compile/T{11635,11719}

comment:6 Changed 16 months ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T11635

comment:7 Changed 16 months ago by bgamari

Description: modified (diff)
Milestone: 8.0.1
Resolution: fixed
Status: mergeclosed
Type of failure: None/UnknownGHC rejects valid program
Last edited 16 months ago by bgamari (previous) (diff)
Note: See TracTickets for help on using tickets.