Empty data declarations are confused with forward data declarations

[dunhamsteve]

Description

This addresses two issues related to confusing empty data declarations with forward data declarations.

The following is accepted by Idris and I believe it should be rejected with an error that Bar is already defined.

data Bar : Type where

data Bar : Type where
    MkBar : Bar

The second issue is that this forward declaration is allowed to be used in an impossible clause and later is defined to not be empty:

data Bar : Type

total
foo : Bar -> a
foo x impossible

data Bar : Type where
    MkBar : Bar

Since forward declarations and empty data appear to be indistinguishable in the data, I added a type flag for forwardDecl. There is an existing flag external that is used in similar cases. This affects serialization, so I updated the TTC version.

The test for elab-util is failing with this PR because it has an empty declaration instead of a forward declaration in one location. I'm filing a PR to address that.

[dunhamsteve]

It looks like this fixes #1083 and #3457

[buzden]

It looks like this fixes #1083 and #3457

#3457 has more complex case than the added case. WDYT, should it also be added as test?

Also, does this change work well for records and their forward declarations? I believe, it should, but I recall some problems with translation of forward declarations of records some time ago.

[dunhamsteve]

Yeah, I'd like to add that case. It's a little more subtle than the other two.

[dunhamsteve]

The record018 test checks that forward declarations of records still work. The following reproduces the issue with record and is fixed by the PR:

record Bar
foo : Bar -> a
foo x impossible
record Bar where
  constructor MkBar

Let me know if you think we should add a test for records. I wouldn't get to it until tomorrow (it's late here).

[gallais]

I personally think a better (but more invasive) fix in terms of modelising what is actually going on
would be to change the type of TCon like so:

  TCon : (tag : Int) -> (arity : Nat) ->
           (parampos : List Nat) -> -- parameters
           (detpos : List Nat) -> -- determining arguments
           (flags : TypeFlags) -> -- should 'auto' implicits check
           (mutwith : List Name) ->
-           (datacons : List Name) ->
+          (datacons : Maybe (List Name)) ->
           (detagabbleBy : Maybe (List Nat)) ->
                    -- argument positions which can be used for
                    -- detagging, if it's possible (to check if it's
                    -- safe to erase)
           Def

0r maybe even (using a yet-to-be-named record rather than the uninformative nested pair of course)

  TCon : (tag : Int) -> (arity : Nat) ->
-           (parampos : List Nat) -> -- parameters
-           (detpos : List Nat) -> -- determining arguments
           (flags : TypeFlags) -> -- should 'auto' implicits check
           (mutwith : List Name) ->
-           (datacons : List Name) ->
+          (dataproperties : Maybe (List Name, List Nat, List Nat, List Nat)) ->
-           (detagabbleBy : Maybe (List Nat)) ->
-                    -- argument positions which can be used for
-                    -- detagging, if it's possible (to check if it's
-                    -- safe to erase)
           Def

and refuse to throw in extra constructors if that Maybe is a Just.

[dunhamsteve]

I'd considered the first option, but went with the less invasive approach. The Maybe (List Name) does model the situation better, forcing us to decide how we want to handle this not-yet-defined situation in each case. I'm looking into that option

I think I've got that working, but want to double check a couple of things after work.

While wiring that through, I saw that positivity checking also assumes the constructors are available. I haven't looked in to it yet, but we may have an issue where a forward declared data type is considered positive.