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 )
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
comment:2 Changed 3 years ago by
Status: | new → merge |
---|---|
Test Case: | → dependent/should_compile/T11719 |
comment:3 Changed 3 years ago by
Description: | modified (diff) |
---|---|
Milestone: | → 8.0.1 |
Resolution: | → fixed |
Status: | merge → closed |
Type of failure: | None/Unknown → GHC rejects valid program |
Merged as 74f760a3dc614ef1354c70e3619130455fb0bdf9.
comment:4 Changed 3 years ago by
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
Resolution: | fixed |
---|---|
Status: | closed → new |
comment:6 Changed 3 years ago by
Keywords: | TypeInType added |
---|
comment:7 Changed 3 years ago by
Milestone: | 8.0.1 → 8.2.1 |
---|
This is out of the scope of 8.0.1 (and perhaps 8.0 entirely).
comment:8 Changed 20 months ago by
Milestone: | 8.2.1 → 8.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
Cc: | Iceland_jack added |
---|
comment:10 Changed 17 months ago by
Cc: | RyanGlScott added |
---|---|
Related Tickets: | → #13913 |
comment:11 Changed 10 months ago by
Milestone: | 8.4.1 → 8.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
Milestone: | 8.6.1 → 8.8.1 |
---|
These won't be fixed for 8.6, bumping to 8.8.
comment:13 Changed 5 weeks ago by
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 follow-ups: 15 17 Changed 5 weeks ago by
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 Changed 5 weeks ago by
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
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>
comment:17 Changed 5 weeks ago by
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 onk
, 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
Cc: | int-index added |
---|
comment:19 Changed 5 weeks ago by
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
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
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
comment:22 Changed 4 weeks ago by
Related Tickets: | #13913 → #13913, #14268 |
---|
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
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
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
Resolution: | → fixed |
---|---|
Status: | new → closed |
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).
In 1701255/ghc: