Option consistency checking bug

[nad]

Consider the following code:

• S.agda:

  {-# OPTIONS --safe --sized-types #-}
  
  module S where
  
  open import Agda.Builtin.Size public

• M.agda:

  {-# OPTIONS --safe #-}
  
  module M where
  
  open import S
  
  f : (i : Size) (j : Size< i) → Size< j → Size< i
  f i j k = k

If I try to load M, then I get a decent error message:

Importing module S not using the --no-sized-types flag from a
module which does.
when scope checking the declaration
  open import S

Let us now add another module in M2.agda:

{-# OPTIONS --safe --sized-types #-}

module M2 where

import S
import M

If I try to load M2, then I get the following error message (for M.agda):

j !=< i of type Size
when checking that the expression k has type Size< i

I would prefer to get an error about the line open import S. Even worse, if f is commented out, then I don't get any error message at all. It seems to me as if there is some bug in the code that checks option consistency.

[fredrikNordvallForsberg]

Do you mean for S to declare the size builtins? Otherwise I don't see how this would work at all.

I will investigate later today.

[nad]

Right, I forgot a line. I've updated the description above.

[nad]

Here is a possibly related bug:

$ cat A.agda
{-# OPTIONS --safe --sized-types #-}

module A where

import B
import C
$ cat B.agda
{-# OPTIONS --safe --sized-types #-}

module B where
$ cat C.agda
{-# OPTIONS --safe #-}

module C where

open import B
$ agda --ignore-interfaces --no-libraries A.agda && echo Success
Checking A ([...]/A.agda).
 Checking B ([...]/B.agda).
 Checking C ([...]/C.agda).
Success
$ agda --no-libraries A.agda && echo Success
Importing module B not using the --no-sized-types flag from a
module which does.

There are two problems: The code should not be accepted the first time, and the error message should include a source location.

[fredrikNordvallForsberg]

Thanks for finding this bug. The possibly related bug was indeed an instance of the same problem, and is also fixed by the commit above:

$ agda --ignore-interfaces --no-libraries A.agda && echo Success
Checking A (/tmp/A.agda).
 Checking B (/tmp/B.agda).
 Checking C (/tmp/C.agda).
/tmp/C.agda:5,1-14
Importing module B not using the --no-sized-types flag from a
module which does.
when scope checking the declaration
  open import B
$ agda --no-libraries A.agda && echo Success
Checking A (/tmp/A.agda).
 Checking C (/tmp/C.agda).
/tmp/C.agda:5,1-14
Importing module B not using the --no-sized-types flag from a
module which does.
when scope checking the declaration
  open import B