#13738 closed bug (fixed)
TypeApplications-related GHC internal error
Reported by: | RyanGlScott | Owned by: | simonpj |
---|---|---|---|
Priority: | normal | Milestone: | 8.4.1 |
Component: | Compiler | Version: | 8.0.1 |
Keywords: | TypeApplications | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | polykinds/T13738 |
Blocked By: | Blocking: | ||
Related Tickets: | #13985 | Differential Rev(s): | |
Wiki Page: |
Description
This is reproducible with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce class MFunctor t where hoist :: (Monad m) => (forall a . m a -> n a) -> t m b -> t n b newtype TaggedTrans tag trans m a = TaggedTrans (trans m a) instance MFunctor trans => MFunctor (TaggedTrans tag trans) where hoist = coerce @(forall (m :: * -> *) (n :: * -> *) (b :: k). Monad m => (forall (a :: *). m a -> n a) -> trans m b -> trans n b) @(forall (m :: * -> *) (n :: * -> *) (b :: k). Monad m => (forall (a :: *). m a -> n a) -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b) hoist
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:18:26: error: • GHC internal error: ‘k’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [a1tR :-> Type variable ‘m’ = m, a1tS :-> Type variable ‘n’ = n, a1tT :-> Type variable ‘b’ = b, a1tV :-> Type variable ‘trans’ = trans, a1tW :-> Type variable ‘tag’ = tag, a1tX :-> Type variable ‘m’ = m, a1tY :-> Type variable ‘n’ = n, a1KE :-> Type variable ‘k’ = k, a1KF :-> Type variable ‘k’ = k] • In the kind ‘k’ In the type ‘(forall (m :: * -> *) (n :: * -> *) (b :: k). Monad m => (forall (a :: *). m a -> n a) -> trans m b -> trans n b)’ In the expression: coerce @(forall (m :: * -> *) (n :: * -> *) (b :: k). Monad m => (forall (a :: *). m a -> n a) -> trans m b -> trans n b) @(forall (m :: * -> *) (n :: * -> *) (b :: k). Monad m => (forall (a :: *). m a -> n a) -> TaggedTrans tag trans m b -> TaggedTrans tag trans n b) hoist | 18 | (b :: k). | ^
Change History (22)
comment:2 Changed 8 months ago by
BTW, this is pretty much the exact code that GHC emits with -ddump-deriv
if you try to write this C (Wrap f)
instance with GeneralizedNewtypeDeriving
:
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE PolyKinds #-} {-# OPTIONS_GHC -ddump-deriv #-} module Works where newtype Wrap f a = Wrap (f a) deriving C class C f where c :: f a
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Works ( Works.hs, interpreted ) ==================== Derived instances ==================== Derived class instances: instance forall k (f :: k -> *). Works.C f => Works.C (Works.Wrap f) where Works.c = GHC.Prim.coerce @(forall (a_a1tD :: k_a1uE). f_a1tE a_a1tD) @(forall (a_a1tD :: k_a1uE). Works.Wrap f_a1tE a_a1tD) Works.c Derived type family instances:
This reveals a pretty-printing bug, as the explicitly quantified kind variable k
referred to by a different name k_a1uE
later.
comment:3 Changed 8 months ago by
There are two workarounds that I'm aware of. One is to explicitly quantify the kind variable k
in the instance declaration:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Coerce import Data.Kind (Type) newtype Wrap f a = Wrap (f a) class C f where c :: f a instance forall k (f :: k -> Type). C f => C (Wrap f) where c = coerce @(forall (a :: k). f a) @(forall (a :: k). Wrap f a) c
(This, of course, requires that you turn on TypeInType
.)
The other workaround is to leave off the kind annotations in the instance altogether:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce newtype Wrap f a = Wrap (f a) class C f where c :: f a instance C f => C (Wrap f) where c = coerce @(forall a. f a) @(forall a. Wrap f a) c
comment:4 Changed 8 months ago by
I've opened #13748 for the issue described in https://ghc.haskell.org/trac/ghc/ticket/13738#comment:2.
comment:5 Changed 6 months ago by
Related Tickets: | → #13985 |
---|
comment:6 Changed 5 months ago by
Another amusing workaround is that you can use a wildcard type in place of k
:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce newtype Wrap f a = Wrap (f a) class C f where c :: f a instance C f => C (Wrap f) where c = coerce @(forall (a :: _). f a) @(forall (a :: _). Wrap f a) c
comment:7 Changed 5 months ago by
Oh dear, I think I've been operating under a misconception in trying to debug this issue. I was originally under the impression that when renaming the expression coerce @(forall (a :: k). f a)
, we would implicitly bind the k
in the forall
type (i.e., it would become something like coerce @(forall k (a :: k). f @k a)
. However, this is decidedly not the case--as the Haddocks for HsAppType
reveal, we use LHsWcType
for representing a visible type argument, precisely because it can have wildcards but not implicit quantification.
In light of this, I think that the original program should actually give a "Not in scope: type variable 'k'"
error. But there's a problem: bindLHsTyVarBndr
always attempts to implicitly bind any free kind variables in forall
'd type variables' kind signatures. As a result, k
never gets reported as out-of-scope after renaming (which would be the ideal way to catch this).
What is the best way to detect this scenario, then? We could add a Bool
argument to bindLHsTyVarBndr
that controls whether it attempts to implicitly bind free kind variables or not. But this feels like a heavy approach, since we'd be tweaking the behavior of a very widely used function in renamer (and causing a lot of replumbing) only to account for LHsWcType
, something which AFAICT is really only used in one particular place: visible type application. But I'm not aware of a more clever way to address this.
comment:8 Changed 5 months ago by
Ah, but wait! I think there's a way to avoid having to replumb tons of functions in the renamer--just repurpose RnTyKiEnv
! We already have a datatype:
data RnTyKiEnv = RTKE { rtke_ctxt :: HsDocContext , rtke_level :: TypeOrKind -- Am I renaming a type or a kind? , rtke_what :: RnTyKiWhat -- And within that what am I renaming? , rtke_nwcs :: NameSet -- These are the in-scope named wildcards }
If I understand the spirit of this type, it would be quite reasonable to augment RTKE
with another filed which indicates whether kind variables in a forall
type should be implicitly quantified or not. If we adopted this approach, then we'd only have to change a couple of call sites, since many of the functions in the renamer already pass around an RnTyKiEnv
argument.
comment:9 Changed 5 months ago by
Differential Rev(s): | → Phab:D3873 |
---|---|
Status: | new → patch |
comment:10 Changed 5 months ago by
I disagree. The RnTyiEnv
is pushed in recursively; and bindLHsTyVarBndrs
is used at every nested forall. But that's not what we want to kind-variable scoping. We only add implicit kind variable binders at the top level of a type signature LHsSigWcType
. We should not be adding any implicit kind-variable bindings at nested foralls.
So
bindLHsTyVarBndrs
has no business binding implicit kind variables at all! It should not be given an argumentkvs
. (Indeed that argument is empty whenbindLHsTyVarBndrs
is invoked by nested foralls.)
bindLHsTyVarBndr
should not be callingbindImplicitKvs
(as it does now). Those kvs should already be in scope, brought into socpe byrn_hs_sig_wc_type
orrnHsSigType
.
- Instead,
bindHsQTyVars
should callrnImplicitBndrs
on the passed-inkv_bndrs
, just asrn_hs_sig_wc_type
does.
Getting rid of this will simplify bindLhsTyVarBndrs
.
And once we have done this, the k
will simply be reported as out of scope.
Does that make sense? Care to have a go?
comment:11 Changed 5 months ago by
Differential Rev(s): | Phab:D3873 |
---|---|
Owner: | set to RyanGlScott |
Thanks for the advice! I'll abandon Phab:D3873 and try again, since the approach you recommend is quite different in spirit.
comment:13 Changed 5 months ago by
Ugh. Trying to change anything involving bindLHsTyVarBndr
is proving to be a massive headache. There are numerous complications here that I'm not sure how to deal with:
- Using
rnImplicitBinders
simply won't work inbindHsQTyVars
.rnImplicitBinders
expects anLHsType GhcPs
as an argument, whichbindHsQTyVars
doesn't have. - Even if we did somehow pass an
LHsType GhcPs
tornImplicitBndrs
frombindHsQTyVars
, I'm not convinced it would do the right thing. The problem: thekv_bndrs
frombindHsQTyVars
need to be bound usingnewTyVarNameRn mb_assoc
(since thekv_bndrs
might be from an associated class), butrnImplicitBndrs
does nothing of the sort. bindLHsTyVarBndr
performs a validity check (here) to ensure that a list of tyvar binders is well scoped (i.e., reject something likeforall (a :: k) k.
). But we can only perform this check becausebindLHsTyVarBndrs
keeps track of the kind variables that are implicitly bound so far, one by one, and communicates this information to each call tobindLHsTyVarBndr
so that it can check if a binder is in the set of implicitly bound kind variables. If we removedbindLHsTyVarBndr
's ability to implicitly bind kind variables, I'm not sure how we'd perform this check at all.- Could we move this error check to
rnImplicitBndrs
? Perhaps, but then we'd need to migrate the code which tracks one-by-one all of the implicitly bound kind variables so far. That doesn't sound fun.
comment:14 Changed 5 months ago by
Owner: | RyanGlScott deleted |
---|
Alas, I bit off way more than I could chew with this ticket. It'll take someone more familiar with the rocket science that powers the renamer to fix this, I think. Unassigning myself as the owner.
comment:18 Changed 5 months ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
Test Case: | → polykinds/T13738 |
OK done! I'd be happy if Richard and/or Ryan wanted to review the changes, but I'm very content with them. A useful step forward.
Oh, and it fixes the ticket.
comment:19 Changed 4 months ago by
Ryan encountered a related regression in 8.2.1, reported as #14209. Perhaps comment:17 should be merged. Unfortunately it's not a terribly small patch. What do you think, Simon?
comment:20 Changed 4 months ago by
Hmm.
- I think that there's an easy source-code workaround for #14209 (correct?), so fixing it isn't that urgent. Leaving 8.2 alone won't block anyone's progress.
- While I doubt the patch will break anything, it is a non-local change so I'm not 100% confident of that claim.
So I'd be inclined to merge it only if we can do a solid smoke-test against all of Hackage/Stackage to confirm the "no-break" claim. In the future that'll be easy to do; I'm not sure how hard it is today.
comment:21 Changed 4 months ago by
FWIW, I didn't notice #14209 in a package in the wild, only when stress-testing different ways of implicitly binding kind variables. And indeed, it doesn have a workaround. Instead of writing this:
{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} module Bug where data MyProxy k (a :: k) = MyProxy data Foo (z :: MyProxy k (a :: k))
You can write this:
{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} module Bug where data MyProxy k (a :: k) = MyProxy data Foo (z :: MyProxy k a)
So I would be OK with not merging that patch.
Here's a somewhat more minimal example: