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

[Andreas Abel]

Frankly, I do not see immediately why the instance for TCErr is in scope 
in module InstanceArguments.

Maybe fix this by adding the import

   import Agda.TypeChecking.Errors ()

to InstanceArguments (hoping this does not create a cycle).

Cheers,
Andreas

On 11.01.2015 19:28, Andrés Sicard-Ramírez wrote:
> 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
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/