Opened 8 months ago

Closed 7 months ago

Last modified 7 months ago

#15116 closed bug (fixed)

GHC internal error when GADT return type mentions its own constructor name

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: GADTs, TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: polykinds/T15116, T15116a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Take the following program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where

data A (a :: k) where
  MkA :: A MkA

On GHC 8.4.2, this is rejected with a sensible error message:

$ /opt/ghc/8.4.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:6:12: error:
    • Data constructor ‘MkA’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the first argument of ‘A’, namely ‘MkA’
      In the type ‘A MkA’
      In the definition of data constructor ‘MkA’
  |
6 |   MkA :: A MkA
  |            ^^^

On GHC HEAD, however, this causes a GHC internal error:

$ ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:6:12: error:
    • GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer
      tcl_env of environment: [asv :-> Type variable ‘k’ = k :: *,
                               asw :-> Type variable ‘a’ = a :: k,
                               rqs :-> ATcTyCon A :: forall k. k -> *]
    • In the first argument of ‘A’, namely ‘MkA’
      In the type ‘A MkA’
      In the definition of data constructor ‘MkA’
  |
6 |   MkA :: A MkA
  |            ^^^

Change History (8)

comment:1 Changed 8 months ago by RyanGlScott

Cc: goldfire added

Commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.) caused this, although it's not obvious to me from a quick glance why this would be the case...

comment:2 Changed 8 months ago by RyanGlScott

Ah, I see what is going on. This is due to the following change in kcLTyClDecl:

 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
   -- See Note [Kind checking for type and class decls]
 kcLTyClDecl (L loc decl)
+  | hsDeclHasCusk decl
+  = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
+  | otherwise
   = setSrcSpan loc $
     tcAddDeclCtxt decl $
-    do { traceTc "kcTyClDecl {" (ppr (tyClDeclLName decl))
+    do { traceTc "kcTyClDecl {" (ppr tc_name)
        ; kcTyClDecl decl
-       ; traceTc "kcTyClDecl done }" (ppr (tyClDeclLName decl)) }
+       ; traceTc "kcTyClDecl done }" (ppr tc_name) }
+  where
+    tc_name = tyClDeclLName decl

Now, if the declaration has a CUSK, then kcTyClDecl is skipped entirely. As a consequence, subsequent checks for each data constructor (kcConDecl) are also skipped. But kcConDecl was what was throwing the error message for the original program, so skipping it leads to pandemonium later down the line.

How should we fix this? I can think of at least a couple of possibilities:

  1. Never skip kcTyClDecl if the declaration has constructors.
  2. Do the kcConDecl checks separately from kcTyClDecl.

Thoughts?

comment:3 Changed 8 months ago by simonpj

I'm on this.

comment:4 Changed 8 months ago by goldfire

Written before Simon's "I'm on this", but I thought it worthy of posting anyway:

I like:

  1. Add the right APromotionErr entries into the env't for tcConDecl.

kcTyClGroup calls getInitialKinds, which returns a NameEnv TcTyThing, mapping names to TcTyThings. Note how TcTyThing includes the APromotionErr constructor (see its definition in TcRnTypes). getInitialKinds not only maps tycon names to TcTyCons (stored in ATcTyCon) but it also maps datacons to APromotionErrs. This is done in getInitialKinds's call to mkPromotionErrorEnv. So, when we look up a datacon in kcTyClDecl, we get a APromotionErr`, just as we should.

Compare to the env't in place for tcTyClDecls, which is built with zipRecTyClss. This env't does not have the APromotionErrs. (See comment above the call to zipRecTyClss.)

The solution is to extend the env't used in type checking to have the APromotionErr entries -- but only for the datacons, not for the tycons (which are no longer errors!). So you'd

This is gnarly code, but this aspect of it isn't as complicated as others. It would make for a good exercise for someone (cough cough) who is working toward becoming an Official Type Checker Grease Monkey.

comment:5 Changed 7 months ago by Simon Peyton Jones <simonpj@…>

In aa03ad88/ghc:

Simplify the kind checking for type/class decls

This patch deletes quite a bit of code,
AND fixes Trac #15116.

comment:6 Changed 7 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T15116, T15116a

Excellent bug report, and provocation to improve. Thanks.

comment:7 Changed 7 months ago by goldfire

For the record, I read this patch and think it's lovely.

comment:8 Changed 7 months ago by simonpj

Thank you!

Note: See TracTickets for help on using tickets.