#13337 closed bug (fixed)
GHC doesn't think a type is of kind *, despite having evidence for it
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.1 |
Component: | Compiler (Type checker) | Version: | 8.0.2 |
Keywords: | TypeInType | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #12677 | Differential Rev(s): | Phab:D3315 |
Wiki Page: |
Description
The easiest way to illustrate this bug is this:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Foo where import Data.Kind (Type) blah :: forall (a :: k). k ~ Type => a -> a blah x = x
$ ghci Foo.hs GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( Foo.hs, interpreted ) Foo.hs:8:43: error: • Expected a type, but ‘a’ has kind ‘k’ • In the type signature: blah :: forall (a :: k). k ~ Type => a -> a
I find this behavior quite surprising, especially since we have evidence that k ~ Type
in scope!
If the program above looks too contrived, consider a similar program that uses Typeable
. I want to write something like this:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Foo where import Data.Kind (Type) import Data.Typeable foo :: forall k (a :: k) proxy. (Typeable k, Typeable a) => proxy a -> String foo _ = case eqT :: Maybe (k :~: Type) of Nothing -> "Non-Type kind" Just Refl -> case eqT :: Maybe (a :~: Int) of Nothing -> "Non-Int type" Just Refl -> "It's an Int!"
This exhibits the same problem. Despite the fact that we pattern-matched on a Refl
of type k :~: Type
, GHC refuses to consider the possibility that a :~: Int
is well kinded, even though (a :: k)
, and we learned from the first Refl
that k ~ Type
!
Change History (18)
comment:1 Changed 14 months ago by
comment:2 Changed 14 months ago by
Forgive me if this is a silly question, but why shouldn't the first example work? I know that the implementation details would significantly complicate the story, but my perspective, being able to write the first example would make a lot of code easier to write. An example of this that came up in real code is when Edward Kmett tried to sketch out a solution to #13327 on the ghc-devs mailing list, and attempted to write this code:
class (Typeable t, Typeable k) => DataIfStar (k :: t) where dataIf :: (t ~ Type) => proxy k -> (Data k => r) -> r
But this won't work, because Data :: Type -> Constraint
, and GHC isn't able to conclude that k :: t
is actually k :: Type
, since the evidence that t ~ Type
isn't being used when typechecking.
If programs like these aren't supposed to typecheck by design, what is the workaround?
comment:3 Changed 14 months ago by
Another way to phrase my question is: I don't see what the distinction between the first and second examples is. After all, you can rewrite the second example like this:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Foo where import Data.Kind (Type) import Data.Typeable foo :: forall k (a :: k) proxy. (Typeable k, Typeable a) => proxy a -> String foo _ = case eqT :: Maybe (k :~: Type) of Nothing -> "Non-Type kind" Just Refl -> go_on eqT where go_on :: k ~ Type => Maybe (a :~: Int) -> String go_on Nothing = "Non-Int type" go_on (Just Refl) = "It's an Int!"
Now the equality assumption isn't coming into scope "only in an expression of that type", it's coming into scope in a type signature! So again, unless I'm misunderstanding something, I strongly suspect that fixing the second program would naturally lend itself towards fixing the first program.
comment:4 Changed 14 months ago by
The problem is that a ~ b
is a lifted type. That is, it contains bottom. So, when you write forall k (a :: k). k ~ Type => a -> a
or some such, there's no place to check whether the proof of k ~ Type
is valid before you use it. When an expression intervenes, then GHC can insert a case
to evaluate the equality proof box to find the real primitive (~#
) equality inside.
Some notes on this issue (intended solely as notes to self, so YMMV) are here.
So I don't agree that solving (2) will help with (1) here.
comment:5 Changed 14 months ago by
Ah, I completely overlooked bottoming equalities. Thanks for the reference.
In light of this, my "equivalent" program in comment:3 is not equivalent at all, since the k ~ Type
evidence in go_on
isn't known a priori to terminate, whereas in the original program, the equality is known not to bottom out by pattern matching on Refl
.
So I suppose a better title for this bug would be "GHC doesn't think a type is of kind *, despite having Typeable-induced evidence for it", and the first program would be related to Dependent Haskell, which is, erm, in progress :)
comment:6 Changed 14 months ago by
Theorem (Progress): For all research projects ρ, either ρ is published, or there exists a day δ such that ρ steps to ρ'.
Proof: Fix a given research project ρ. We now have two cases: either ρ is published, which trivially implies progress; or we must produce a day δ in which ρ will advance. We are done, choosing δ = tomorrow. QED.
So, yes, Dependent Haskell is in progress. And, yes, I agree with your other analysis in comment:5.
comment:7 Changed 14 months ago by
Richard and I discussed the bug mentioned in comment:1. Solution
Don't do solveEqualities unless you are generalising (to solve #13337), in tc_hs_sig_type
Richard will work on this.
comment:8 Changed 14 months ago by
Owner: | set to goldfire |
---|
Included in that work should be a check of all uses of solveEqualities
to make sure that they make sense.
comment:9 Changed 14 months ago by
Keywords: | TypeInType added |
---|
comment:10 Changed 14 months ago by
Differential Rev(s): | → Phab:D3315 |
---|---|
Status: | new → patch |
comment:11 Changed 14 months ago by
Milestone: | → 8.2.1 |
---|
comment:13 Changed 13 months ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
Merged to ghc-8.2
as 109a2429493c2a2d5481b67f5b0c1086a959813e.
comment:14 Changed 13 months ago by
Status: | closed → merge |
---|
Modified by
commit 3cfee57abf00f794e7962e2a60efd9d7d8baf06f Author: Richard Eisenberg <rae@cs.brynmawr.edu> Date: Thu Mar 16 15:56:37 2017 -0400 Remove solveSomeEqualities I had thought that it was necessary to solve kind-level equalities before validity-checking a type, but I was wrong. This patch simply deletes code. Hooray!
Has this been merged?
comment:15 Changed 13 months ago by
Status: | merge → closed |
---|
Indeed, that was merged to ghc-8.2
as 6c41ed6e7994451f78af87bff43d6baef19b8f0f.
comment:17 Changed 13 months ago by
Not worth merging this to the 8.2 branch, I think. It's just refactoring.
comment:18 Changed 10 months ago by
Related Tickets: | → #12677 |
---|
See #12677 for a proper ticket devoted to the (k ~ Type)
issue.
For your first example: this infelicity is by design, though I can't find documentation in the manual. Equality assumptions (such as your
k ~ Type
) come into scope only in an expression of that type, not later on in the same type. This design significantly eased the implementation.The second example should work -- that's a bug.