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