[GHC] #15116: GHC internal error when GADT return type mentions its own constructor name

3 May 2018


      #15116: GHC internal error when GADT return type mentions its own constructor name
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  GADTs,         |  Operating System:  Unknown/Multiple
  TypeInType                         |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Take the following program:

 {{{#!hs
 {-# 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
   |            ^^^
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15116
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler