Opened 6 months ago

Closed 3 months ago

Last modified 2 months ago

#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:1 Changed 6 months ago by RyanGlScott

Here's a somewhat more minimal example:

{-# 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 :: k). f a)
             @(forall (a :: k). Wrap f a)
      c
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
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:15:29: error:
    • GHC internal error: ‘k’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [a1tN :-> Type variable ‘a’ = a,
                               a1tQ :-> Type variable ‘f’ = f, a1uU :-> Type variable ‘k’ = k]
    • In the kind ‘k’
      In the type ‘(forall (a :: k). f a)’
      In the expression:
        coerce @(forall (a :: k). f a) @(forall (a :: k). Wrap f a) c
   |
15 |   c = coerce @(forall (a :: k). f a)
   |
Last edited 6 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 6 months ago by RyanGlScott

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 6 months ago by RyanGlScott

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
Last edited 6 months ago by RyanGlScott (previous) (diff)

comment:4 Changed 6 months ago by RyanGlScott

I've opened #13748 for the issue described in https://ghc.haskell.org/trac/ghc/ticket/13738#comment:2.

comment:5 Changed 4 months ago by RyanGlScott

comment:6 Changed 3 months ago by RyanGlScott

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 3 months ago by RyanGlScott

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 3 months ago by RyanGlScott

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 3 months ago by RyanGlScott

Differential Rev(s): Phab:D3873
Status: newpatch

comment:10 Changed 3 months ago by simonpj

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 argument kvs. (Indeed that argument is empty when bindLHsTyVarBndrs is invoked by nested foralls.)
  • bindLHsTyVarBndr should not be calling bindImplicitKvs (as it does now). Those kvs should already be in scope, brought into socpe by rn_hs_sig_wc_type or rnHsSigType.
  • Instead, bindHsQTyVars should call rnImplicitBndrs on the passed-in kv_bndrs, just as rn_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 3 months ago by RyanGlScott

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:12 Changed 3 months ago by simonpj

Terrific, thank you! I'll gladly review

comment:13 Changed 3 months ago by RyanGlScott

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 in bindHsQTyVars. rnImplicitBinders expects an LHsType GhcPs as an argument, which bindHsQTyVars doesn't have.
  • Even if we did somehow pass an LHsType GhcPs to rnImplicitBndrs from bindHsQTyVars, I'm not convinced it would do the right thing. The problem: the kv_bndrs from bindHsQTyVars need to be bound using newTyVarNameRn mb_assoc (since the kv_bndrs might be from an associated class), but rnImplicitBndrs 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 like forall (a :: k) k.). But we can only perform this check because bindLHsTyVarBndrs keeps track of the kind variables that are implicitly bound so far, one by one, and communicates this information to each call to bindLHsTyVarBndr so that it can check if a binder is in the set of implicitly bound kind variables. If we removed bindLHsTyVarBndr'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 3 months ago by RyanGlScott

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:15 Changed 3 months ago by goldfire

This is in my area. I'll take a look in due course.

comment:16 Changed 3 months ago by simonpj

Owner: set to simonpj

I'm 99% through this. I'll commit shortly.

comment:17 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In 0257dacf/ghc:

Refactor bindHsQTyVars and friends

This work was triggered by Trac #13738, which revealed to me that
the code RnTypes.bindHsQTyVars and bindLHsTyVarBndrs was a huge
tangled mess -- and outright wrong on occasion as the ticket showed.

The big problem was that bindLHsTyVarBndrs (which is invoked at every
HsForAll, including nested higher rank ones) was attempting to bind
implicit kind variables, which it has absolutely no busineess doing.
Imlicit kind quantification is done at the outside only, in fact
precisely where we have HsImplicitBndrs or LHsQTyVars (which also
has implicit binders).

Achieving this move was surprisingly hard, because more and more
barnacles had accreted aroud the original mistake.  It's much
much better now.

Summary of changes.  Almost all the action is in RnTypes.

* Implicit kind variables are bound only by
  - By bindHsQTyVars, which deals with LHsQTyVars
  - By rnImplicitBndrs, which deals with HsImplicitBndrs

* bindLHsTyVarBndrs, and bindLHsTyVarBndr are radically simplified.
  They simply does far less, and have lots their forest of
  incomprehensible accumulating parameters.  (To be fair, some of
  the code in bindLHsTyVarBndrs just moved to bindHsQTyVars, but
  in much more perspicuous form.)

* The code that checks if a variable appears in both a kind and
  a type (triggering RnTypes.mixedVarsErr) was bizarre.  E.g.
  we had this in RnTypes.extract_hs_tv_bndrs
       ; check_for_mixed_vars bndr_kvs acc_tvs
       ; check_for_mixed_vars bndr_kvs body_tvs
       ; check_for_mixed_vars body_tvs acc_kvs
       ; check_for_mixed_vars body_kvs acc_tvs
       ; check_for_mixed_vars locals body_kvs
  I cleaned all this up; now we check for mixed use at binding
  sites only.

* Checks for "Variable used as a kind before being bound", like
     data T (a :: k) k = rhs
  now just show up straightforwardly as "k is not in scope".
  See Note [Kind variable ordering]

* There are some knock-on simplifications in RnSource.

comment:18 Changed 3 months ago by simonpj

Resolution: fixed
Status: patchclosed
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 2 months ago by bgamari

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 2 months ago by simonpj

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 2 months ago by RyanGlScott

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.

comment:22 Changed 2 months ago by bgamari

Milestone: 8.4.1

Let's not merge in that case.

Note: See TracTickets for help on using tickets.