[GHC] #9590: AMP breaks `haskell2010` package
GHC
ghc-devs at haskell.org
Mon Feb 16 16:39:47 UTC 2015
#9590: AMP breaks `haskell2010` package
-------------------------------------+-------------------------------------
Reporter: hvr | Owner: ekmett
Type: bug | Status: closed
Priority: high | Milestone: 7.10.1
Component: Core Libraries | Version: 7.9
Resolution: fixed | Keywords: AMP,
Operating System: Unknown/Multiple | report-impact
Type of failure: GHC rejects | Architecture:
valid program | Unknown/Multiple
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions: Phab:D510
-------------------------------------+-------------------------------------
Comment (by hvr):
Agda seems to have support via pragmas to inform the compiler about
desugaring primitives (citing
https://pay.reddit.com/r/haskell/comments/2vzqqa/picking_your_prelude/comxs6z):
> Agda has a nice mechanism for avoiding this problem. The
compiler/typechecker uses various functions and constants that are not
built in to the language: for instance rewriting requires
`PropositionalEquality` and its `refl` constructor, and desugaring
numerals requires knowledge of the natural number type and the `zero` and
`suc` constructors.
>
> All of these are made known to the Agda system in the standard library
with a pragma:
{{{
{-# LANGUAGE BUILTIN REFL refl #-}
{-# LANGUAGE BUILTIN ZERO zero #-}
}}}
> etc.
>
> It's then possible to completely throw out the standard library and
replace it with one of your own by using these pragmas to tell Agda to use
your definitions instead.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9590#comment:20>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list