[GHC] #15152: Core Lint error in ill-typed GADT code

14 May 2018

      #15152: Core Lint error in ill-typed GADT code
-------------------------------------+-------------------------------------
           Reporter:  tdammers       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #11066
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}

 module T3651 where

 data Z a where
   U :: Z ()
   B :: Z Bool

 unsafe2 :: a ~ b => Z b -> Z a -> a
 unsafe2 B U = ()
 }}}

 On current GHC HEAD, this fails with an "Inaccessible branch" error.
 However, if we turn this error into a warning, e.g. using the following
 patch:

 {{{
 --- a/compiler/typecheck/TcErrors.hs
 +++ b/compiler/typecheck/TcErrors.hs
 @@ -708,7 +708,7 @@ mkGivenErrorReporter implic ctxt cts
                               Nothing ty1 ty2

         ; traceTc "mkGivenErrorReporter" (ppr ct)
 -       ; maybeReportError ctxt err }
 +       ; reportWarning NoReason err }
    where
      (ct : _ )  = cts    -- Never empty
      (ty1, ty2) = getEqPredTys (ctPred ct)
 }}}

 ...and then compile with `-dcore-lint -Werror`, the program gets rejected
 with a core lint error:

 {{{
 [1 of 1] Compiling T3651            ( minimal.hs, minimal.o )
 *** Core Lint errors : in result of Desugar (before optimization) ***
 <no location info>: warning:
     In a case alternative: (U co_a1ri :: (a_a1rd :: *) ~# (() :: *))
     Unfilled coercion hole: {co_a1rw}
 <no location info>: warning:
     In a case alternative: (U co_a1ri :: (a_a1rd :: *) ~# (() :: *))
     co_a1rw :: (() :: *) ~# (Bool :: *)
     [LclId[CoVarId]] is out of scope
 *** Offending Program ***
 Rec {
 $tcZ :: TyCon
 [LclIdX]
 $tcZ
   = TyCon
       5287023927886307113##
       7998054209879401454##
       $trModule
       (TrNameS "Z"#)
       0#
       krep$*Arr*

 $tc'U :: TyCon
 [LclIdX]
 $tc'U
   = TyCon
       5625905484817226555##
       8662083060712566586##
       $trModule
       (TrNameS "'U"#)
       0#
       $krep_a1sr

 $tc'B :: TyCon
 [LclIdX]
 $tc'B
   = TyCon
       477146386442824276##
       11145321492051770584##
       $trModule
       (TrNameS "'B"#)
       0#
       $krep_a1st

 $krep_a1sr [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a1sr
   = KindRepTyConApp $tcZ (: @ KindRep $krep_a1ss ([] @ KindRep))

 $krep_a1st [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a1st
   = KindRepTyConApp $tcZ (: @ KindRep $krep_a1su ([] @ KindRep))

 $krep_a1ss [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a1ss = KindRepTyConApp $tc() ([] @ KindRep)

 $krep_a1su [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a1su = KindRepTyConApp $tcBool ([] @ KindRep)

 $trModule :: Module
 [LclIdX]
 $trModule = Module (TrNameS "main"#) (TrNameS "T3651"#)

 unsafe2 :: forall a b. ((a :: *) ~ (b :: *)) => Z b -> Z a -> a
 [LclIdX]
 unsafe2
   = \ (@ a_a1rd)
       (@ b_a1re)
       ($d~_a1rg :: (a_a1rd :: *) ~ (b_a1re :: *)) ->
       let {
         $d~~_a1ro :: (a_a1rd :: *) ~~ (b_a1re :: *)
         [LclId]
         $d~~_a1ro = $p1~ @ * @ a_a1rd @ b_a1re $d~_a1rg } in
       case heq_sel @ * @ * @ a_a1rd @ b_a1re $d~~_a1ro of co_a1rp
       { __DEFAULT ->
       \ (ds_d1sv :: Z b_a1re) (ds_d1sw :: Z a_a1rd) ->
         let {
           fail_d1tc :: Void# -> a_a1rd
           [LclId]
           fail_d1tc
             = \ (ds_d1td [OS=OneShot] :: Void#) ->
                 patError
                   @ 'LiftedRep @ a_a1rd "minimal.hs:12:1-16|function
 unsafe2"# } in
         case ds_d1sv of wild_00 {
           __DEFAULT -> fail_d1tc void#;
           B co_a1rh ->
             let {
               co_a1ru :: (a_a1rd :: *) ~# (Bool :: *)
               [LclId[CoVarId]]
               co_a1ru = CO: co_a1rp ; co_a1rh } in
             case ds_d1sw of wild_00 {
               __DEFAULT -> fail_d1tc void#;
               U co_a1ri ->
                 ()
                 `cast` (Sub ({co_a1rw} ; Sym co_a1ru)
                         :: (() :: *) ~R# (a_a1rd[sk:2] :: *))
             }
         }
       }
 end Rec }

 *** End of Offense ***

 <no location info>: error:
 Compilation had errors

 }}}

 However, without core linting, the correct errors appear:

 {{{
 [1 of 1] Compiling T3651            ( minimal.hs, minimal.o )

 minimal.hs:12:1: error: [-Woverlapping-patterns, -Werror=overlapping-
 patterns]
     Pattern match has inaccessible right hand side
     In an equation for ‘unsafe2’: unsafe2 B U = ...
    |
 12 | unsafe2 B U = ()
    | ^^^^^^^^^^^^^^^^

 minimal.hs:12:11: error: [-Werror]
     • Couldn't match type ‘Bool’ with ‘()’
       Inaccessible code in
         a pattern with constructor: U :: Z (), in an equation for
 ‘unsafe2’
     • In the pattern: U
       In an equation for ‘unsafe2’: unsafe2 B U = ()
    |
 12 | unsafe2 B U = ()
    |           ^
 }}}

 Without either core linting or `-Werror`, GHC just emits the warnings, and
 then falls into a hole:

 {{{
 [1 of 1] Compiling T3651            ( minimal.hs, minimal.o )

 minimal.hs:12:1: warning: [-Woverlapping-patterns]
     Pattern match has inaccessible right hand side
     In an equation for ‘unsafe2’: unsafe2 B U = ...
    |
 12 | unsafe2 B U = ()
    | ^^^^^^^^^^^^^^^^

 minimal.hs:12:11: warning:
     • Couldn't match type ‘Bool’ with ‘()’
       Inaccessible code in
         a pattern with constructor: U :: Z (), in an equation for
 ‘unsafe2’
     • In the pattern: U
       In an equation for ‘unsafe2’: unsafe2 B U = ()
    |
 12 | unsafe2 B U = ()
    |           ^
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.5.20180508 for x86_64-unknown-linux):
         opt_univ fell into a hole
   {co_a1rw}
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in
 ghc:Outputable
         pprPanic, called at compiler/types/OptCoercion.hs:242:5 in
 ghc:OptCoercion

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
 }}}

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

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)