Opened 6 months ago
Last modified 12 days 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: | 8.8.1 |
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 (13)
comment:1 Changed 6 months ago by
comment:2 Changed 6 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 6 months ago by
Cc: | Iceland_jack added |
---|
comment:4 Changed 6 months ago by
That patch is held up on the #12919 patch, which is under review at Phab:D4451.
comment:5 Changed 5 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 4 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 4 months 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.
comment:8 Changed 3 weeks ago by
Milestone: | → 8.8.1 |
---|
comment:10 Changed 3 weeks ago by
Principle: implicitly-quantified variables always precede explicitly-quantified variables in a type or kind. So Foo1
and Foo2
in the OP are not equivalent.
- In
Foo1
the implicitly-quantified variables arek
anda::k
; and GHC can put them in that order. - But in
Foo2
the implicitly quantified variable is onlya::k
and that can't come first.
comment:11 Changed 3 weeks ago by
Richard's patch says
"The error message for dependent/should_fail/TypeSkolEscape has become noticeably worse. However, this is because the code in TcErrors goes to some length to preserve pre-8.0 error messages for kind errors. It's time to rip off that plaster and get rid of much of the kind-error-specific error messages. I tried this, and doing so led to a lovely error message for TypeSkolEscape. So: I'm accepting the error message quality regression for now, but will open up a new ticket to fix it, along with a larger error-message improvement I've been pondering. This applies also to dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142."
We think this is related.
comment:12 Changed 3 weeks ago by
I think the best way to get good error messages here is to bring both implicit and explicit variables into scope all at once, and then have setImplicationStatus
report errors involving both explicit and implicit variables. See Note [Keeping scoped variables in order: Explicit]
in TcHsType for the general idea; here, I'm proposing this plan to cover implicit variables, too.
One wrinkle: datatypes go via a different mechanism, in kcLHsQTyVars
and friends. Question: could we unify these mechanisms?
comment:13 Changed 12 days ago by
I've found another bizarre case where implicitly quantifying a kind variable works, but explicitly quantifying it does not. Consider the following program:
{-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} module Bug where import Data.Proxy f :: forall (x :: a). Proxy (x :: _) f = Proxy
This typechecks, but if I change the type signature of f
to explicitly quantify a
:
f :: forall a (x :: a). Proxy (x :: _)
Then it no longer typechecks! Here is the error you get an a somewhat recent GHC HEAD build:
GHCi, version 8.7.20180802: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:9:32: error: • Expected kind ‘a’, but ‘x’ has kind ‘a1’ • In the first argument of ‘Proxy’, namely ‘(x :: _)’ In the type ‘Proxy (x :: _)’ In the type signature: f :: forall a (x :: a). Proxy (x :: _) | 9 | f :: forall a (x :: a). Proxy (x :: _) | ^
Do you think that this shares a symptom in common with the other programs mentioned in this ticket? (Or is this a separate bug?)
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!