[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
GHC
ghc-devs at haskell.org
Wed Apr 4 08:28:56 UTC 2018
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.2
checker) | Keywords: TypeInType,
Resolution: | TypeFamilies,
| PartialTypeSignatures, TypedHoles
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: #13877 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
I regret to report that even after Richard's "solveEqualties" patch
#14066, the example in comment:2 yields
{{{
T14040.hs:91:28: error:ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180402 for x86_64-unknown-linux):
No skolem info:
[a1_aWV[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in
ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in
ghc:TcErrors
}}}
This arises during the error-report-generation stage. The residual
constraint is this
{{{
reportUnsolved (after zonking):
Free tyvars: (t_a1e3[tau:2] :: Proxy x_a1dP[sk:2]) a_aWV[sk:1]
Tidy env: ([ESf6y :-> 1, ESf7a :-> 1, ESfO0 :-> 2,
ESgiS :-> 1],
[aWV :-> a1_aWV[sk:1], a1dP :-> x_a1dP[sk:2],
a1dQ :-> a_a1dQ[sk:2], a1e3 :-> t0_a1e3[tau:2]])
Wanted: WC {wc_impl =
Implic {
TcLevel = 2
Skolems = (x_a1dP[sk:2] :: a_aWV[sk:1])
a_a1dQ[sk:2]
(f_a1dR[sk:2] :: forall (x :: a_a1dQ[sk:2]).
Proxy x ~> *)
(x_a1dS[sk:2] :: a_a1dQ[sk:2])
No-eqs = True
Status = Unsolved
Given =
Wanted =
WC {wc_simple =
[D] _ {0}:: Sing t_a1e3[tau:2]
-> Sing
(Apply
(f_a1dR[sk:2] x_a1dP[sk:2])
t_a1e3[tau:2]) (CHoleCan:
TypeHole(_))}
Binds = EvBindsVar<a2gv>
Needed inner = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
:-> co_a2hR,
a2hS :-> co_a2hS, a2i2 :-> $dIP_a2i2]
Needed outer = [a2hM :-> co_a2hM, a2hN :-> co_a2hN,
a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR
:-> co_a2hR,
a2hS :-> co_a2hS]
the type signature for:
dapp :: forall (x :: a_aWV[sk:1]) a (f :: forall (x ::
a).
Proxy x ~>
*) (x :: a).
Sing (f x) -> Sing x -> f x @@ 'Proxy }
}}}
And indeed you can see that the skolem `a1_aWV` is not bound by any
implication. This must be a bug.
Richard?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14040#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list