MAlonzo yields peculiar scope errors

[UlfNorell]

From co...@strictlypositive.org on October 25, 2013 19:00:27

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). A friend managed to install Agda to take my Metaprogramming course. After a lot of cabal brutality, he brought up my Basics.agda file into emacs and then hit "compile" rather than "load". Bad things happened. So I poked about a bit and did some shrinking. Here's a thing which produces the symptoms.

module BugAlonzo where

postulate
      Level : Set
      lzero  : Level
      lsuc   : Level -> Level
      lmax   : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX  lmax   #-}

record Sg {l : Level}(S : Set l)(T : S -> Set l) : Set l where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public

data Two : Set where tt ff : Two
_<?>_ : forall {l}{P : Two -> Set l} -> P tt -> P ff -> (b : Two) -> P b
(t <?> f) tt = t
(t <?> f) ff = f

_+_ : Set -> Set -> Set
S + T = Sg Two (S <?> T)

MAlonzo (i.e., ghc) responds

Compilation error:

/Users/conor/Desktop/AgdaBook/MetaprogAgda/MAlonzo/Code/BugAlonzo.hs:24:34:
    Not in scope: `d2'
    Perhaps you meant one of these:
      `d8' (line 6), `d28' (line 22), `d23' (line 31)

/Users/conor/Desktop/AgdaBook/MetaprogAgda/MAlonzo/Code/BugAlonzo.hs:26:42:
    Not in scope: `d3'
    Perhaps you meant one of these:
      `d8' (line 6), `d23' (line 31), `d1' (line 41)

/Users/conor/Desktop/AgdaBook/MetaprogAgda/MAlonzo/Code/BugAlonzo.hs:26:68:
    Not in scope: `d2'
    Perhaps you meant one of these:
      `d8' (line 6), `d28' (line 22), `d23' (line 31) What version of Agda are you using? On what operating system (if relevant)? 2.3.2.1 on a Mac, but the same symptoms were reported on a Linux box

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

[UlfNorell]

From andreas....@gmail.com on October 25, 2013 16:00:13

Hitting "Compile" is not safe, so don't do this at home. Agda's warranty is for type-checking only. ;-)

All 3 compilers have been abandoned by their makers, so I wonder not if they refuse to work.

But concerning the concrete issue, I get another error with Agda 2.3.3:

Compilation error:

/home/abel/tmp/Agda2/test/bugs/MAlonzo/Code/ Issue925 .hs:1:1: The function main' is not defined in moduleMAlonzo.Code. Issue925 '

Which seems fair. Command-line compilation works fine as well:

abel@agda:~/tmp/Agda2/test/bugs$ ghc -c MAlonzo/Code/ Issue925 .hs

MAlonzo/Code/ Issue925 .hs:16:1: Warning: Pattern match(es) are overlapped In an equation for `d14': d14 v0 = ...

MAlonzo/Code/ Issue925 .hs:45:1: Warning: Pattern match(es) are overlapped In an equation for `d15': d15 v0 = ...

Maybe this is a problem that has been fixed already.

Status: InfoNeeded
Labels: Type-Defect Compiler

[UlfNorell]

From co...@strictlypositive.org on October 26, 2013 01:44:22

Certainly, "no main" is a more intelligible response. I'm thinking of doing some FFI stuff with my undergrads, and am now afraid that a reinstall may prove necessary. Thanks for looking into it.

[UlfNorell]

From andreas....@gmail.com on October 27, 2013 06:57:13

Closing this. Feel free to reopen if problem persists.

Status: Invalid
Owner: andreas....@gmail.com