Suboptimal constraint solving
Here a summary of -ddump-tc-trace
for this program (part of test T12427a)
data T where
T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
h11 y = case y of T1 _ v -> v
I see this sequence
{co_awA} {0}:: ((forall b. [b] -> [b]) -> Int)
~# p_awz[tau:1] (CNonCanonical)
==> Hetero equality gives rise to kind equality
inert: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
work item: {co_awF} :: 'GHC.Types.LiftedRep ~# p_awy[tau:1]
co_awA := Sym ({co_awG} ; Sym (GRefl nominal ((forall b.[b] -> [b]) -> Int)
(TYPE {co_awF})_N))
==> Swap awF, kick out awG
work item: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
inert (because p_awy is untouchable):
{co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
co_awF := Sym co_awH
==> flatten awG (strange double GRefl)
inert: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awG := {co_awI} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N)
; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE {co_awF})_N)
at this point we also make a derived shadow of awI, for some reason.
Solving stops here, but we float out awI, and awH, and then have another go
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
work: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awI (why?)
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awI := {co_awJ} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N) ; GRefl nominal ((forall b. [b] -> [b])
-> Int)
(TYPE (Sym {co_awH}))_N)
==> solve awH: p_awy := LiftedRep, kick out awJ
{co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awJ
co_awJ := {co_awK} ; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N
{co_awK} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int)
This seems like we are doing too much work, esp the double GRefls. Why did awI get flattened?
It's not a disaster, but pretty heavy handed.