[GHC] #15152: Core Lint error in ill-typed GADT code
GHC
ghc-devs at haskell.org
Mon May 14 15:02:52 UTC 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
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
More information about the ghc-tickets
mailing list