[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