Display form/pragma bugs

[GoogleCodeExporter]

Bug-helper.agda:

module Bug-helper where

record Record : Set₁ where
  field _≡_ : {A : Set} → A → A → Set

module Module (r : Record) where

  open Record r public

Bug.agda:

module Bug where

open import Bug-helper

module M (r : Record) where

  open Module r

  postulate
    A   : Set
    a b : A

  Foo : a ≡ b
  Foo = {!!}

-- Bug 1
-- -----
--
-- The goal is displayed in a nice way if Agda is restarted and
-- Bug.agda is loaded:
--
--   ?0 : a ≡ b
--
-- However, if Bug.agda is reloaded, then we get the following result:
--
--   ?0 : (r Record.≡ a) b

-- Bug 2
-- -----
--
-- Let's try to work around the bug by adding a DISPLAY pragma just
-- before Foo:
--
--   {-# DISPLAY Record._≡_ _ x y = x ≡ y #-}
--
-- Result if the module is first loaded without the pragma and is then
-- reloaded with the pragma:
--
--   ?0 : _≡_ b
--
-- Result if the module is reloaded again:
--
--   ?0 : (r Record.≡ a) b
--
-- Result if Agda is restarted and the module is loaded:
--
--   ?0 : a ≡ b
--
-- If "open Module r" is replaced by "open Record r", then the last
-- result above is replaced by the following one:
--
--   ?0 : _≡_ b
--
-- In case it is relevant: I have disabled sharing.

Original issue reported on code.google.com by nils.anders.danielsson on 29 Apr 2015 at 4:40

[GoogleCodeExporter]

The DisplayForm gets added to the stImports field, since it goes
Bug-helper.Record.≡ --> Bug.M._.≡.

And stImports is not in the part of the state that gets restored.

I'm not sure whether it should.

Original comment by sanzhi...@gmail.com on 4 Jun 2015 at 11:21

[GoogleCodeExporter]

Fixed the part about (r Record.≡ a)

ec24023

Original comment by sanzhi...@gmail.com on 5 Jun 2015 at 10:39

[GoogleCodeExporter]

-- Another example:

postulate
  I : Set
  P : I → Set

record R (i : I) : Set₁ where
  field
    _∙_ : P i → P i → Set

module M₁ where

  postulate
    r : (i : I) → R i
    i : I
    x : P i

  open module M₂ {i : I} = R (r i)

  foo : x ∙ x
  foo = ?

-- The goal type is x ∙ x. Good!
--
-- The normalised goal type is (r i R.∙ x) x. Bad! (Can this be
-- improved without the use of display pragmas?)
--
-- Let's try to fix this using the following display pragma, placed
-- just before foo:
--
--   {-# DISPLAY R._∙_ _ x y = x ∙ y #-}
--
-- Now both the goal type and the normalised goal type are x ∙ x.
-- Good!
--
-- Let's now add a parameter to M₁:
--
--   module M₁ (X : Set) where
--
-- The goal type is still x ∙ x. Good! However, the normalised goal
-- type is _∙_ x. Very bad!
--
-- Yet another example:

postulate
  I : Set
  P : I → Set

record R (i : I) : Set₁ where
  field
    _∙_ : P i → P i → Set

module M₂ (r : (i : I) → R i) where

  postulate
    i : I
    x : P i

  open module M₃ {i : I} = R (r i)

  {-# DISPLAY _∙_ _ x y = x ∙ y #-}

  foo : x ∙ x
  foo = ?

-- The goal type is _∙_ x. Very bad! The normalised goal type is
-- (r i R.∙ x) x. Bad!
--
-- It seems as if display pragmas don't work properly inside
-- parametrised modules.

Original comment by nils.anders.danielsson on 6 Jun 2015 at 1:25

[UlfNorell]

This is working as intended. Display pragma right-hand sides are checked in the empty context (i.e. outside the module telescope), so if you want to use names from a parameterised module in the right-hand side of a display pragma you need to supply values for the module parameters as well. If you didn't it's not at all clear what to do outside the module. For instance,

postulate
  F : Set → Set
  D : Set

module M (A : Set) where

  postulate G : Set → Set
  {-# DISPLAY F X = G X #-}  -- this should be F X = G e X, for some e, but if it wasn't...

  foo : F A
  foo = {!!}  -- ...and we wanted this to print as G A

open M

bar : F D
bar = {!!}   -- then what do we do here? G ?? A