coerce can cause compiler to loop

This program causes GHC to loop at compile time

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Coerce
coerce' :: Coercible b a => a -> b
coerce' = coerce (\x -> x :: b) :: forall a b. Coercible b a => a -> b

I encountered this trying to use a similar construction in

https://github.com/glguy/profunctors/blob/coerce/src/Data/Profunctor/Unsafe.hs

I'm not absolutely certain about what aspect of this snippet is looping the compiler, but it's pretty small.

Trac metadata

Trac field	Value
Version	7.10.1-rc1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

JFTR, this does not loop with 7.8.4, so it is likely related to the Coercible solver rewrite.

Trac metadata

Trac field	Value
CC	→ goldfiere

assigned to @rae

Richard, might you look at this?

Confirmed with GHC HEAD.

Here is the repeating tail of -ddump-tc-trace (not sure if it is useful)

updWorkList
  WL {Eqs = [G] cobox_am7 :: Coercible
                               b_am6[sk] a_am5[sk] (CTyEqCan)}
Start solver pipeline {
  work item =  [G] cobox_am7 :: Coercible
                                  b_am6[sk] a_am5[sk] (CTyEqCan)
  inerts    =  Equalities: [G] cobox_amr :: Coercible
                                              b_amq[sk] a_amp[sk] (CTyEqCan)
               Type-function equalities:
               Dictionaries:
               Irreds:
               Insolubles = {}
               Solved dicts
runStage canonicalization {
  workitem   =  [G] cobox_am7 :: Coercible
                                   b_am6[sk] a_am5[sk] (CTyEqCan)
canEqTyVar
  b_am6[sk]
  a_am5[sk]
  Not-swapped
flattenTyVar1
  a_am5[sk]
  *
canEqTyVar flat LHS
  b_am6[sk]
  b_am6[sk]
  a_am5[sk]
  Not-swapped
  a_am5[sk]
end stage canonicalization }
runStage interact with inerts {
  workitem   =  [G] cobox_am7 :: Coercible
                                   b_am6[sk] a_am5[sk] (CTyEqCan)
Can't solve tyvar equality
  LHS: b_am6[sk] :: *
  RHS: a_am5[sk] :: *
  TcLevel = 3
Kick out, tv = b_am6[sk]
  n-kicked = 1
  n-kept fun-eqs = 0
  WL {Eqs = [G] cobox_amr :: Coercible
                               b_amq[sk] a_amp[sk] (CTyEqCan)}
end stage interact with inerts }
1832[U:3<C:0,F:0>] Kept as inert (1 kicked out):
    [G] cobox_am7 :: Coercible b_am6[sk] a_am5[sk]
End solver pipeline (discharged) }
  inerts = Equalities: [G] cobox_am7 :: Coercible
                                          b_am6[sk] a_am5[sk] (CTyEqCan)
           Type-function equalities:
           Dictionaries:
           Irreds:
           Insolubles = {}
           Solved dicts
updWorkList
  WL {Eqs = [G] cobox_amr :: Coercible
                               b_amq[sk] a_amp[sk] (CTyEqCan)}

Thanks to glguy for such a nice, tiny test case and to Joachim (nomeata) for the dump. I'm able to solve this without testing! Just add a critical missing not in the bowels of kick_out. Will validate and push shortly.

Just using Phab to validate... I don't think this needs external eyes to review.

Trac metadata

Trac field	Value
Differential revisions	→ D630

mentioned in commit cecf036f

Please merge for 7.10.1. This is a clear error and should be dead simple to merge. Thanks!

Trac metadata

Trac field	Value
Test case	→ typecheck/should_compile/T10031

added 1 deleted label

closed

changed milestone to %7.10.1

Merged to ghc-7.10 (via 2387369c).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added compiler crash label

added Pnormal label