reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs
reOrient _untch (VarCls tv1) (FunCls {}) = not $ isMetaTyVar tv1
+ -- Put function on the left, *except* if the RHS becomes
+ -- a meta-tyvar; see invariant on CFunEqCan
+ -- and Note [No touchables as FunEq RHS]
-reOrient _untch (VarCls tv1) (FskCls {}) = not $ isMetaTyVar tv1
- -- See Note [Loopy Spontaneous Solving, Example 4]
+reOrient _untch (VarCls tv1) (FskCls {}) = not $ isMetaTyVar tv1
+ -- Put flatten-skolems on the left if possible:
+ -- see Note [Loopy Spontaneous Solving, Example 4] in TcInteract
reOrient _untch (VarCls {}) (OtherCls {}) = False
reOrient _untch (VarCls {}) (VarCls {}) = False
reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2
- -- See Note [Loopy Spontaneous Solving, Example 4]
+ -- See Note [Loopy Spontaneous Solving, Example 4] in TcInteract
reOrient _untch (FskCls {}) (FskCls {}) = False
reOrient _untch (FskCls {}) (FunCls {}) = True
, sr_stop = ContinueWith workItem }
Just (workItem', workList')
- | not (isGivenCt workItem) -- Original was wanted or derived but we have now made him
- -- given so we have to interact him with the inerts due to
- -- its status change. This in turn may produce more work.
- -> do { (new_inert, new_work) <- runSolverPipeline [ ("recursive interact with inert eqs", interactWithInertEqsStage)
- , ("recursive interact with inerts", interactWithInertsStage)
- ] inerts workItem'
- ; return $ SR { sr_new_work = new_work `unionWorkLists` workList'
+ | not (isGivenCt workItem)
+ -- Original was wanted or derived but we have now made him
+ -- given so we have to interact him with the inerts due to
+ -- its status change. This in turn may produce more work.
+ -- We do this *right now* (rather than just putting workItem'
+ -- back into the work-list) because we've solved
+ -> do { (new_inert, new_work) <- runSolverPipeline
+ [ ("recursive interact with inert eqs", interactWithInertEqsStage)
+ , ("recursive interact with inerts", interactWithInertsStage)
+ ] inerts workItem'
+ ; return $ SR { sr_new_work = new_work `unionWorkLists` workList'
, sr_inerts = new_inert -- will include workItem'
, sr_stop = Stop }
- }
+ }
| otherwise
-> -- Original was given; he must then be inert all right, and
-- workList' are all givens from flattening
-- * tv not in tvs(xi) (occurs check)
-- * If constraint is given then typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
- -- * if @xi@ is a flatten skolem then @tv@ can only be:
+ -- * If 'xi' is a flatten skolem then 'tv' can only be:
-- - a flatten skolem or a unification variable
-- i.e. equalities prefer flatten skolems in their LHS
- -- See Note [Loopy Spontaneous Solving, Example 4]
- -- Also related to [Flatten Skolem Equivalence Classes]
+ -- See Note [Loopy Spontaneous Solving, Example 4]
+ -- Also related to [Flatten Skolem Equivalence Classes]
cc_id :: EvVar,
cc_flavor :: CtFlavor,
cc_tyvar :: TcTyVar,