Skip to content

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

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
  |            ^^^
Trac metadata
Trac field Value
Version 8.5
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information