#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