Opened 4 months ago
Last modified 8 weeks ago
#14887 new bug
Explicitly quantifying a kind variable causes a telescope to fail to kind-check
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.2.2 |
Keywords: | TypeInType | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
Consider the following program:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fprint-explicit-kinds #-} module Bug where import Data.Kind import Data.Type.Equality type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where Foo1 (e :: a :~: a) = a :~: a type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where Foo2 k (e :: a :~: a) = a :~: a
Foo2
is wholly equivalent to Foo1
, except that in Foo2
, the k
kind variable is explicitly quantified. However, Foo1
typechecks, but Foo2
does not!
$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:13:10: error: • Couldn't match kind ‘k’ with ‘k1’ When matching the kind of ‘a’ Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’ • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ In the type family declaration for ‘Foo2’ | 13 | Foo2 k (e :: a :~: a) = a :~: a | ^^^^^^^^^^^^^^
(Moreover, there seems to be a tidying bug, since GHC claims that (:~:) k a a
is not the same kind as (:~:) k a a
.)
Change History (7)
comment:1 Changed 4 months ago by
comment:2 Changed 4 months ago by
Owner: | set to goldfire |
---|
Interesting bug, thanks. But not much point in looking at this until Richard's "solveEqualities" patch lands. Richard?
comment:3 Changed 4 months ago by
Cc: | Iceland_jack added |
---|
comment:4 Changed 4 months ago by
That patch is held up on the #12919 patch, which is under review at Phab:D4451.
comment:5 Changed 3 months ago by
The #12919 patch has landed. Interestingly, the program in comment:1 now gives a different error:
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180403: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:10:43: error: • Expected kind ‘k’, but ‘a’ has kind ‘k0’ • In the first argument of ‘Proxy’, namely ‘(a :: k)’ In the kind ‘Proxy (a :: k)’ | 10 | type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {} | ^
comment:6 Changed 2 months ago by
Keywords: | TypeFamilies removed |
---|---|
Summary: | Explicitly quantifying a kind variable causes a type family to fail to typecheck → Explicitly quantifying a kind variable causes a telescope to fail to kind-check |
As it turns out, this is not at all specific to type families. The same phenomenon occurs in data types:
data Foo1 (e :: Proxy (a :: k)) :: Type -- typechecks data Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type -- doesn't typecheck
Or even plain old functions:
foo1 :: forall (e :: Proxy (a :: k)). Int -- typechecks foo1 = 42 foo2 :: forall (k :: Type) (e :: Proxy (a :: k)). Int -- doesn't typecheck foo2 = 42
So I'm guessing that any type variable telescope suffers from this issue.
comment:7 Changed 8 weeks ago by
Here's what is going on with:
foo2 :: forall (k :: Type) (e :: Proxy (a :: k)). Int
In TcHsType.tc_hs_sig_type_and_gen
we see
tc_hs_sig_type_and_gen skol_info (HsIB { hsib_vars = sig_vars , hsib_body = hs_ty }) kind = do { (tkvs, ty) <- solveEqualities $ tcImplicitTKBndrs skol_info sig_vars $ tc_lhs_type typeLevelMode hs_ty kind
Here sig_vars
is just a
. Now tcImplicitTKBndrs
gives a
a kind k0
(a unification variable), so
we attempt to kind-check
forall (a::k0). forall (k :: Type) (e :: Proxy (a :: k)). Int
But that requires k0 ~ k
, which is a skolem-escape problem. We end up trying (and failing) solve
the constraint
Implic { TcLevel = 2 Skolems = (a_avH[sk:2] :: k_aZs[tau:2]) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = k_aZp[sk:3] (e_aZq[sk:3] :: Proxy k_aZp[sk:3] (a_avH[sk:2] |> {co_aZC})) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_simple = [WD] hole{co_aZC} {0}:: (k_aZs[tau:2] :: *) GHC.Prim.~# (k_aZp[sk:3] :: *) (CNonCanonical)}
Here k0
is k_aZs
, and it is (rightly) untouchable inside the level-3 implication.
Hence the error message.
I have not yet thought about what to do. Richard may have some ideas.
A slight twist on this is if you leave out the type family equations. For instance:
Foo1
typechecks, butFoo2
does not:I have no idea why GHC is complaining about the scoping order here—that looks well-scoped to me!