Opened 19 months ago

Last modified 3 months ago

#11719 new bug

Cannot use higher-rank kinds with type families

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

Description (last modified by bgamari)

This ticket came out of a discussion with Richard in this mailing list post: https://mail.haskell.org/pipermail/haskell-cafe/2016-March/123462.html

Here's the code that should work, but doesn't:

import Data.Kind

data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *

type family (f :: a ~> b) @@ (x :: a) :: b

data Null a = Nullable a | NotNullable a

type family ((f :: b ~> c)  (g :: a ~> b)) (x :: a) :: c where
  (f  g) x = f @@ (g @@ x)

type family BaseType (k :: forall a. a ~> Type) (x :: b) :: Type where   -- this fails :(
--  BaseType k x = (@@) k x

Change History (10)

comment:1 Changed 18 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:2 Changed 18 months ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T11719

comment:3 Changed 18 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 18 months ago by bgamari (previous) (diff)

comment:4 Changed 18 months ago by ocharles

I see this ticket is now marked as "fixed", but the original code example above doesn't type check under this change (as Richard's commit message mentions). Should this ticket be re-opened, or should I open a new ticket?

comment:5 Changed 18 months ago by simonpj

Resolution: fixed
Status: closednew

comment:6 Changed 18 months ago by simonpj

Keywords: TypeInType added

comment:7 Changed 17 months ago by bgamari

Milestone: 8.0.18.2.1

This is out of the scope of 8.0.1 (and perhaps 8.0 entirely).

comment:8 Changed 6 months ago by bgamari

Milestone: 8.2.18.4.1

Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

comment:9 Changed 4 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 3 months ago by RyanGlScott

Cc: RyanGlScott added
Note: See TracTickets for help on using tickets.