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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11066            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by bgamari):

 * cc: simonpj (added)


Old description:

> 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
> }}}
New description:

 Consider the following program:

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

 {{{#!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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11066            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by tdammers:

Old description:

> Consider the following program:
>
> {{{#!hs
> {-# 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:
>
> {{{#!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
> }}}
New description:

 Consider the following program:

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

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

 This behavior also appears in the following test cases from the GHC test
 suite:

 - `gadt/T3651`
 - `gadt/T7558`

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15152#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11066            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by tdammers):

 The discussion in this earlier attempt at solving #11066 might prove
 relevant also: https://phabricator.haskell.org/D1454#42098?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15152#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11066            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"f49f90bb84b12515366de9b8184644b5c3798901/ghc" f49f90b/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="f49f90bb84b12515366de9b8184644b5c3798901"
 Tidy up error suppression

 Trac #15152 showed that when a flag turned an error into a warning, we
 were still (alas) suppressing subequent errors; includign their
 essential addTcEvBind.  That led (rightly) to a Lint error.

 This patch fixes it, and incidentally tidies up an ad-hoc special
 case of out-of-scope variables (see the old binding for
 'out_of_scope_killer' in 'tryReporters').

 No test, because the problem was only shown up when turning
 inaccessible code into a warning.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15152#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#15152: Core Lint error in ill-typed GADT code
-------------------------------------+-------------------------------------
        Reporter:  tdammers          |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.2
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11066            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => closed
 * resolution:   => fixed


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15152#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets