[GHC] #15577: TypeApplications-related infinite loop (GHC 8.6+ only)
GHC
ghc-devs at haskell.org
Fri Aug 31 18:38:56 UTC 2018
#15577: TypeApplications-related infinite loop (GHC 8.6+ only)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: high | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) | Keywords:
Resolution: | TypeApplications, TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
performance bug | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
I know what is happening here. In `TcCanonical.canCFunEqCan` we have
{{{
canCFunEqCan ev fn tys fsk
= do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys
-- cos :: tys' ~ tys
; let lhs_co = mkTcTyConAppCo Nominal fn cos
-- :: F tys' ~ F tys
new_lhs = mkTyConApp fn tys'
flav = ctEvFlavour ev
; (ev', fsk')
-- See Note [canCFunEqCan]
<- if isTcReflCo kind_co
then
..normal, homo-kinded case..
else
..hetero-kinded case..
...
}}}
The note is a good explanation; read it.
In the example above, we get a Given `CFunEqCan` ''that is homo-kinded''.
But `kind_co` turns out not to be `ReflCo` but rather some giant (but
still reflexive)
coercion. ''So we fall ito the heter-kinded case''.
Then, as the Note says, we make a new homo-kinded `CFunEqCan`. But
when we end up processing that (as we do), we think it too is hetero-
kinded,
and so we do it all over again. Forever.
For now I have fixed it by using `isTcReflexiveCo` instead of
`isTcReflCo`.
But isn't it suspicious that `flattenArgsNom` returns a complicated giant
coercion?
And that gets right back into `flatten_args_fast` and `flatten_args_slow`,
which
we were discussing last week. I'll leave that for Richard and Ningning to
ponder.
Meanwhile I think I have fixed the loop. Validating now....
Here for completeness is part of the log
{{{
canCFunEqCan: non-refl
Kind co: (Sym (GRefl nominal (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
; ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(Sym ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal
f_a28k[sk:1] {co_a28p})
->_N <*>_N))) ; (Sym (GRefl nominal
a_a28l[sk:1]
(({co_a29i} ; ((Sym
(GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N
<*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))) ; GRefl nominal a_a28l[sk:1]
(({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)))) (Sym (GRefl nominal (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl
nominal f_a28k[sk:1]
{co_a28p})
(Sym (Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p}))) ; (Sym (GRefl nominal r_a28m[sk:1]
(Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
{co_a28p})) ; GRefl nominal r_a28m[sk:1]
(Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
{co_a28p})))
RHS: fsk_a29k[fsk:2] :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)) ;
((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal
f_a28k[sk:1]
{co_a28p})
LHS: F (f_a28k[sk:1] |> {co_a28p})
(a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1]
{co_a28p}) ; GRefl
nominal f_a28k[sk:1] {co_a28p})
->_N <*>_N)) ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
{co_a28p})
r_a28x[tau:1]
:: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal
f_a28k[sk:1]
{co_a28p}) ; GRefl
nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)) ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
{co_a28p})
New LHS F (f_a28k[sk:1] |> {co_a28p})
(a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal
f_a28k[sk:1]
{co_a28p}) ; GRefl
nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)) ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1]
{co_a28p})
r_a28x[tau:1]
:: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal
f_a28k[sk:1]
{co_a28p}) ; GRefl
nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N)) ; ((Sym (GRefl
nominal f_a28k[sk:1]
{co_a28p}) ; GRefl nominal f_a28k[sk:1]
{co_a28p})
->_N <*>_N))
(r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal
f_a28k[sk:1]
{co_a28p})
}}}
This shows stuff right at the start of the hetero-kinded 'else' branch
above
* `kind_co` is the giant coercion returned by `flattenArgsNom`
* `RHS` is the fsk, and I show its kind, which is `(a |> ..) (r |> ..)`
* `LHS` is the original function application, `(F tys)` in the code above;
again I show its kind, which is identical to that of fks.
* `New LHS` is the new function application after flattening, `(F tys')`
in the code. You'll note that it is '''identical''' to `(F tys)`!
All this work for nothing. Surely `flattenArgsNom` can be a bit cleverer?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15577#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list