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

[Andreas Abel]

I considered this, but does import {-# SOURCE #-} really mean to just 
include the file?  I thought it is a regular import of an .hs-boot file.
I might not understand how instances are imported.

Maybe it would be good to alert the Haskell developers to this 
incompatibility.

On 12.01.2015 04:53, Andrés Sicard-Ramírez wrote:
>
> On 11 January 2015 at 18:03, Andreas Abel <abela at chalmers.se
> <mailto:abela at chalmers.se>> wrote:
>
>     Frankly, I do not see immediately why the instance for TCErr is in
>     scope in module InstanceArguments.
>
>
> ​I found the reason. The module InstanceArguments imports the modules
>
>    import {-# SOURCE #-} Agda.TypeChecking.Constraints
>    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
>    import {-# SOURCE #-} Agda.TypeChecking.Conversion
>
> and either one of these modules imports the module TypeChecking.Errors
> which defines the required instance.
> ​
> ​So, there is an issue in GHC 7.10.1 RC1.
>
> --
> 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/