[Agda-dev] Mysterious instance: GHC 7.10.1 RC1 bug? GHC <= 7.8.4 bug?

[Andrés Sicard-Ramírez]

Hi,

The function

  handle :: TCErr -> TCM Bool
  handle err = do
    reportSDoc "tc.instance" 50 $
      text "assignment failed:" <+> prettyTCM err
     return False

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).


In the master branch, GHC 7.10.1 RC1 yields the error

src/full/Agda/TypeChecking/InstanceArguments.hs:349:43:
    No instance for (PrettyTCM TCErr) arising from a use of ‘prettyTCM’
    In the second argument of ‘(<+>)’, namely ‘prettyTCM err’
    In the second argument of ‘($)’, namely
      ‘text "assignment failed:" <+> prettyTCM err’
    In a stmt of a 'do' block:
      reportSDoc "tc.instance" 50
      $ text "assignment failed:" <+> prettyTCM err

but using GHC <= 7.8.4, the module compiles without problems.

Is the instance of PrettyTCM for TCErr in scope in the module
TypeChecking.InstanceArguments? Why?

​Best,​

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150111/24dbbe5d/attachment.html