Opened 3 years ago

Closed 3 weeks ago

#11719 closed bug (fixed)

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, int-index, csongor.kiss14@…, s.eisenbach@…, t.field@…
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, #14268 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 (25)

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 3 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 3 years ago by simonpj

Resolution: fixed
Status: closednew

comment:6 Changed 3 years ago by simonpj

Keywords: TypeInType added

comment:7 Changed 3 years 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 20 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 18 months ago by Iceland_jack

Cc: Iceland_jack added

comment:10 Changed 17 months ago by RyanGlScott

Cc: RyanGlScott added

comment:11 Changed 10 months ago by bgamari

Milestone: 8.4.18.6.1

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 5 months ago by bgamari

Milestone: 8.6.18.8.1

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

comment:13 Changed 5 weeks ago by RyanGlScott

Is this another consequence of this limitation? Consider the following program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

type family Sing :: k -> Type

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True
type instance Sing = SBool

sFalse :: Sing False
sFalse = SFalse

This typechecks without issue. However, if you change the following line of code:

type family Sing :: k -> Type

To become this:

type family Sing :: forall k. k -> Type

Then it stops typechecking:

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:18:10: error:
    • Couldn't match type ‘SBool’ with ‘Sing’
      Expected type: Sing 'False
        Actual type: SBool 'False
    • In the expression: SFalse
      In an equation for ‘sFalse’: sFalse = SFalse
   |
18 | sFalse = SFalse
   |          ^^^^^^

I find this extremely surprising: I would have thought that GHC could treat type family Sing :: k -> Type and type family Sing :: forall k. k -> Type identically without the need for any fancy higher-rank business (like what the original program in this ticket requires).

comment:14 Changed 5 weeks ago by goldfire

These two declarations have quite different meanings:

type family F1 :: k -> Type
type family F2 :: forall k. k -> Type

F1 takes one argument, k. F2, on the other hand, takes no arguments. F1 can match on k, returning constructors of different kinds in different instances. On the other hand, F2 must return a polykinded constructor, and can have only one instance.

So, I think this is unrelated to the ticket...

comment:15 in reply to:  14 Changed 5 weeks ago by RyanGlScott

Replying to goldfire:

On the other hand, F2 must return a polykinded constructor, and can have only one instance.

That doesn't appear to be true, since this program (with multiple F2 instances) typechecks:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

type family F2 :: forall k. k -> Type
type instance F2 = SBool
type instance F2 = STuple0

data SBool :: Bool -> Type where
  SFalse :: SBool False
  STrue  :: SBool True
data STuple0 :: () -> Type where
  STuple0 :: STuple0 '()

comment:16 Changed 5 weeks ago by Iceland_jack

It works on HEAD but fails on 8.2.1 (after adding {-# LANGUAGE TypeInType #-}), regression?

$ ghci -ignore-dot-ghci 504.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Bug              ( 504.hs, interpreted )

504.hs:12:20: error:
    • Expected kind ‘forall k. k -> *’,
        but ‘SBool’ has kind ‘Bool -> *’
    • In the type ‘SBool’
      In the type instance declaration for ‘F2’
   |
12 | type instance F2 = SBool
   |                    ^^^^^

504.hs:13:20: error:
    • Expected kind ‘forall k. k -> *’,
        but ‘STuple0’ has kind ‘() -> *’
    • In the type ‘STuple0’
      In the type instance declaration for ‘F2’
   |
13 | type instance F2 = STuple0
   |                    ^^^^^^^
Failed, 0 modules loaded.
Prelude> 
Last edited 5 weeks ago by Iceland_jack (previous) (diff)

comment:17 in reply to:  14 Changed 5 weeks ago by int-index

Replying to goldfire:

These two declarations have quite different meanings:

type family F1 :: k -> Type
type family F2 :: forall k. k -> Type

This statement doesn't sit well with me. I expect to be able to introduce any type variable explicitly, and F1 with an explicit forall for k turns out to be F2. These declarations must have the same meaning.

Let's compare to term-level functions:

f :: k -> Type
f :: forall k. k -> Type

These types are the same (modulo specificity of k)!

F1 takes one argument, k. F2, on the other hand, takes no arguments. F1 can match on k, returning constructors of different kinds in different instances. On the other hand, F2 must return a polykinded constructor, and can have only one instance.

So you mean that we treat F1 as having kind pi k. k -> Type, while F2 has kind forall k. k -> Type: F1 can match on its parameter k and F2 cannot. Why? I thought we always treat forall as pi in kinds, at least for now.

Therefore, I agree with Ryan's expectations in comment:13.

comment:18 Changed 5 weeks ago by int-index

Cc: int-index added

comment:19 Changed 5 weeks ago by goldfire

The difference with terms is that the arity of type families matters. F1 has arity 1, while F2 has arity 0. The real question is: where is the k bound. In F1, k is bound "before the colon", while in F2, it's bound after the colon.

In terms of this syntax:

F1 :: foreach k  . k -> Type
F2 :: foreach k '. k -> Type

Both are really foreach-kinds, like @int-index observed. The difference is that F1's argument is not matchable. (Perversely, type families can pattern-match only on unmatchable arguments. Perhaps a name change is in order.) On the other hand, F2's argument is matchable, as it's declared to be so. (Recall that every abstraction in a kind is currently interpreted as matchable, even though the future syntax for matchable kinds will change.)

Accepting the program in comment:15 seems like an egregious bug, to me. I've reported it as #15740.

comment:20 Changed 5 weeks ago by simonpj

Cc: csongor.kiss14@… s.eisenbach@… t.field@… added

The difference with terms is that the arity of type families matters. F1 has arity 1, while F2 has arity 0. The real question is: where is the k bound. In F1, k is bound "before the colon", while in F2, it's bound after the colon.

Tricky stuff! Could we document this in the user manual?

If we end up adopting Csongor's ideas about unsaturated type families (when the matchability shows up in the kind), we'll need to adopt some notation for the forall-case too.

I can't say I like forall k '. k -> Type! But we clearly need something.

Perversely, type families can pattern-match only on unmatchable arguments. Perhaps a name change is in order.

That is indeed perverse. Worth considering as part of the same effort.

comment:21 Changed 4 weeks ago by Iceland_jack

Something to consider (I don't know if I got the typing right, but allowing higher rank kinds in splitting type application)

type RudeWord a = 
  forall xx. xx -> a

type family
  Split (a :: res) :: forall arg. Maybe (RudeWord res, arg) where
  Split ((f :: RudeWord res) @arg (a :: arg)) = 'Just '(f, a)
  Split _                                     = 'Nothing
Last edited 4 weeks ago by Iceland_jack (previous) (diff)

comment:22 Changed 4 weeks ago by RyanGlScott

I've found a workaround for the original issue in this ticket after much persistence. The trick is to associate BaseType with a type class:

class CBaseType (k :: forall a. a ~> Type) (x :: b) where
  type BaseType k x :: Type

Then, define a flexible instance like so, using an explicit forall to give k the appropriate higher-rank kind:

instance forall b (k :: forall a. a ~> Type) (x :: b). CBaseType k x where
  type BaseType k x = (@@) k x

That's it! Now you can use BaseType like you'd expect:

λ> data ProxySym0 :: forall a. a ~> Type
λ> type instance ProxySym0 @@ x = Proxy x
λ> :kind! BaseType ProxySym0 Bool
BaseType ProxySym0 Bool :: *
= Proxy Bool
λ> :kind! BaseType ProxySym0 Maybe
BaseType ProxySym0 Maybe :: *
= Proxy Maybe
λ> :kind! BaseType ProxySym0 'Just
BaseType ProxySym0 'Just :: *
= Proxy 'Just

It's a bit gnarly, but this is the best that you can do until #14268 is implemented.

comment:23 Changed 3 weeks ago by RyanGlScott

Now that #14268 is implemented, we can work around this issue in a much less hacky way:

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

That being said, the way that I originally thought this type family should have been defined:

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

Still does not kind-check:

$ ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:22:13: error:
    • Expected kind ‘forall a. a ~> *’, but ‘k’ has kind ‘a0 ~> *’
    • In the first argument of ‘BaseType’, namely
        ‘(k :: forall a. a ~> Type)’
      In the type family declaration for ‘BaseType’
   |
22 |   BaseType (k :: forall a. a ~> Type) x = (@@) k x
   |             ^

This feels like it ought to Just Work™, though. Should we keep this ticket open until this is possible?

comment:24 Changed 3 weeks ago by goldfire

comment:23 is a feature request. The use of a type variable in a type family equation -- even on the left-hand side -- is an occurrence, not a binding site. Type families aren't functions! So I think it's OK as is, myself.

Someday, we'll just have type-level functions, and then all of this will be better. :)

comment:25 Changed 3 weeks ago by RyanGlScott

Resolution: fixed
Status: newclosed

Alright, you've convinced me. In that case, let's close this ticket. (We can always open a new one in the event that we want to accept the program in comment:23).

Note: See TracTickets for help on using tickets.