#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/comxs6...):
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