<div dir="ltr"><div class="gmail_default" style="font-size:small">Hi,<br><br></div><div class="gmail_default" style="font-size:small">The function<br><br> handle :: TCErr -> TCM Bool<br> handle err = do<br> reportSDoc "tc.instance" 50 $<br> text "assignment failed:" <+> prettyTCM err<br> return False<br><br></div><div class="gmail_default" style="font-size:small">in the module TypeChecking.InstanceArguments requires an instance of PrettyTCM for TCErr. This instance is defined in the module TypeChecking.Errors (note that this is an orphan instance).<br><br></div><div class="gmail_default" style="font-size:small"><br>In the master branch, GHC 7.10.1 RC1 yields the error<br><br>src/full/Agda/TypeChecking/InstanceArguments.hs:349:43:<br> No instance for (PrettyTCM TCErr) arising from a use of ‘prettyTCM’<br> In the second argument of ‘(<+>)’, namely ‘prettyTCM err’<br> In the second argument of ‘($)’, namely<br> ‘text "assignment failed:" <+> prettyTCM err’<br> In a stmt of a 'do' block:<br> reportSDoc "tc.instance" 50<br> $ text "assignment failed:" <+> prettyTCM err<br><br></div><div class="gmail_default" style="font-size:small">but using GHC <= 7.8.4, the module compiles without problems.<br><br></div><div class="gmail_default" style="font-size:small">Is the instance of PrettyTCM for TCErr in scope in the module TypeChecking.InstanceArguments? Why?<br></div><br><div class="gmail_default" style="font-size:small">Best,</div><br>-- <br><div class="gmail_signature"><div dir="ltr">Andrés<br></div></div>
</div>