Commit 8737d47e authored by dimitris's avatar dimitris
Browse files

When rewriting a flavor with rewriteCtFlavor, in the case of reflexivity,

avoid setting the flavor PredType to be the new PredType if the types exactly
match, so that in case of failure we report errors that do not have expanded
type synonyms.
parent d29e2776
......@@ -1418,11 +1418,17 @@ rewriteCtFlavor_cache _cache (Derived wl _pty_orig) pty_new _co
rewriteCtFlavor_cache cache fl pty co
| isTcReflCo co
-- If just reflexivity then you may re-use the same variable as optimization
= return (Just $ case fl of
Derived wl _pty_orig -> Derived wl pty
Given gl ev -> Given gl (setVarType ev pty)
Wanted wl ev -> Wanted wl (setVarType ev pty)
Solved gl ev -> Solved gl (setVarType ev pty))
= if ctFlavPred fl `eqType` pty then
-- E.g. for type synonyms we want to use the original type
-- since it's not flattened to report better error messages.
return $ Just fl
else
-- E.g. because we rewrite with a spontaneously solved one
return (Just $ case fl of
Derived wl _pty_orig -> Derived wl pty
Given gl ev -> Given gl (setVarType ev pty)
Wanted wl ev -> Wanted wl (setVarType ev pty)
Solved gl ev -> Solved gl (setVarType ev pty))
| otherwise
= xCtFlavor_cache cache fl [pty] (XEvTerm ev_comp ev_decomp) cont
where ev_comp [x] = mkEvCast x co
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment