Opened 3 years 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.8.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:

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 (12)

comment:1 Changed 3 years 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 3 years ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T11719

comment:3 Changed 3 years ago by bgamari

Description: modified (diff)
Milestone: 8.0.1
Resolution: fixed
Status: mergeclosed
Type of failure: None/UnknownGHC rejects valid program
Last edited 3 years ago by bgamari (previous) (diff)

comment:4 Changed 2 years 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 2 years ago by simonpj

Resolution: fixed
Status: closednew

comment:6 Changed 2 years ago by simonpj

Keywords: TypeInType added

comment:7 Changed 2 years ago by bgamari


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

comment:8 Changed 18 months ago by bgamari


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

comment:9 Changed 16 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 15 months ago by RyanGlScott

Cc: RyanGlScott added

comment:11 Changed 8 months ago by bgamari


This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:12 Changed 3 months ago by bgamari


These won't be fixed for 8.6, bumping to 8.8.

Note: See TracTickets for help on using tickets.