Missing level primitives in MAlonzo

[UlfNorell]

From guillaum...@gmail.com on June 06, 2013 21:26:53

{- The program below gives the following error when trying to compile it (using MAlonzo)

$ agda -c Test.agda Checking Test (/tmp/Test.agda). Finished Test. Compiling Test in /tmp/Test.agdai to /tmp/MAlonzo/Code/Test.hs Calling: ghc -O -o /tmp/Test -Werror -i/tmp -main-is MAlonzo.Code.Test /tmp/MAlonzo/Code/Test.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns [1 of 2] Compiling MAlonzo.RTE ( MAlonzo/RTE.hs, MAlonzo/RTE.o ) [2 of 2] Compiling MAlonzo.Code.Test ( /tmp/MAlonzo/Code/Test.hs, /tmp/MAlonzo/Code/Test.o )

Compilation error:

/tmp/MAlonzo/Code/Test.hs:21:35: Not in scope: d5' Perhaps you meant one of these: d1' (line 11), d4' (line 26),d9' (line 29)

-}

{- Here is the program -}

module Test where

data ℕ : Set where O : ℕ S : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-} {-# BUILTIN ZERO O #-} {-# BUILTIN SUC S #-}

postulate ULevel : Set zero : ULevel suc : ULevel → ULevel max : ULevel → ULevel → ULevel

{-# BUILTIN LEVEL ULevel #-} {-# BUILTIN LEVELZERO zero #-} {-# BUILTIN LEVELSUC suc #-} {-# BUILTIN LEVELMAX max #-}

postulate IO : ∀ {i} → Set i → Set i return : ∀ {i} {A : Set i} → A → IO A

{-# BUILTIN IO IO #-}

main : IO ℕ main = return (S 1)

{- It’s the first time I try to compile an Agda program, so presumably I’m doing something wrong. But even if I’m doing something wrong, Agda should be the one giving the error, not ghc. -}

Original issue: http://code.google.com/p/agda/issues/detail?id=867

[UlfNorell]

From nils.anders.danielsson on June 06, 2013 14:29:19

You can get the module to compile by adding the following postulates (at least the first two):

{-# COMPILEDTYPE ULevel () #-} {-# COMPILED zero () #-} {-# COMPILED suc ( -> ()) #-} {-# COMPILED max ( -> ()) #-}

If you then try to run the compiled program it will crash, perhaps in the following way:

Test: MAlonzo Runtime Error: postulate evaluated: Test.return

The release notes for Agda 2.3.0 document one way in which one can handle a universe-polymorphic IO constructor.

I don't know of anyone who is inclined to spend much time on error reporting for the FFI, so don't expect too much. Perhaps it's not too hard to change the name "d5" into something like "d_zero". Would this be good enough for you?

(If anyone is eager to provide a patch: The module Agda.Compiler.MAlonzo.Encode contains code that turns Agda module names into lexically valid Haskell module names.)

Status: InfoNeeded
Labels: Type-Enhancement Priority-Medium Compiler ErrorReporting

[UlfNorell]

From guillaum...@gmail.com on June 06, 2013 14:55:09

Thanks, adding those four lines make it crash like you said, which is more reasonable. But why doesn’t the original program crash with an error like the following?

Test: MAlonzo Runtime Error: postulate evaluated: Test.zero

[UlfNorell]

From nils.anders.danielsson on June 10, 2013 07:54:39

But why doesn’t the original program crash with an error like the following?

Good point. I think it should.

Internally Agda treats the level constructors (zero, suc, max) as primitives with "primClauses = Just []", and because the list is empty no code is generated for these constructors. I don't know if this is indicative of an internal error, or if it is intended, but I think someone should look into this.

Status: Accepted
Labels: -Type-Enhancement -Priority-Medium Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From andreas....@gmail.com on June 15, 2013 07:42:13

Somehow the level operations are internally handled as primitives, not as simply builtin postulates. I guess this is because we want(ed) to calculate with them. I do not know, but I think some implementation details about levels are outdated. E.g. I found a comment in Builtin.hs saying "TODO: make max [meaning levelmax] a postulate". Anyway, Nisse has found the source of the error, which took me one hour to also find it. The fix is simple. I guess, MAlonzo does not expect "Just []" to be a valid set of clauses. I handle this case now as if "Nothing" was given for primClauses. Also, I added primitive Haskell implementation of the level operations into MAlonzo.

Nisse, since you had found the bug, you could have fixed it as well... ;-) The competent ones for this, Ulf and Makoto, are not really active...

Summary: Missing level primitives in MAlonzo (was: GHC error when trying to compile a program)
Status: Fixed
Owner: andreas....@gmail.com
Labels: -ErrorReporting Builtin

[UlfNorell]

From nils.anders.danielsson on June 17, 2013 02:44:42

Nisse, since you had found the bug, you could have fixed it as well... ;-)

I didn't want to fix the bug through yet another hack (a special case in MAlonzo). Are you sure that this problem doesn't affect other compiler backends? I don't know all the details, but having "primClauses = Just []" seems problematic, so I think we should address the source of the problem, not just this particular symptom.

Status: InfoNeeded

[UlfNorell]

From andreas....@gmail.com on June 17, 2013 02:46:39

Maybe primClauses should just be a list, with [] taking the role of Nothing. I do not see why Just [] is meaningful...

[UlfNorell]

From nils.anders.danielsson on June 17, 2013 03:04:49

If you plan to change anything, please find out what it is that generates "Just []" before you implement the change.

[UlfNorell]

From andreas....@gmail.com on June 17, 2013 09:37:23

The culprit was in TypeChecking/Rules/Builtin.bindPostulatedName:

  BuiltinPrim pfname axioms -> do
case e of
  A.Def qx -> do

        PrimImpl t pf <- lookupPrimitiveFunction pfname
        v <- checkExpr e t

        axioms v

        info <- getConstInfo qx
        let cls = defClauses info
            a   = defAbstract info
            mcc = defCompiled info
        bindPrimitive pfname $ pf { primFunName = qx }
        addConstant qx $ info { theDef = Primitive a pfname (Just cls) mcc }

        -- needed? yes, for checking equations for mul
        bindBuiltinName s v

Apparently, the invariant that primFunName is used iff primClauses==Nothing was not supposed to hold!? I think now it is clearer, that we fall back to primFunName if there are null primClauses.

Pushed a patch that removes the Maybe from primClauses.

Status: Fixed