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.

[dunhamsteve]

I've updated this to use Maybe (List Name). To avoid breaking elab reflection, it will return an empty List in the case of Nothing for getCons. I've given it a different ttcVersion. Because TCon has changed, the lsp will need to be updated after this patch.

[gallais]

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.

We seem to be okay:

%default total

data Negation : Type -> Type

failing "Absurd is not total, not strictly positive"

  data Absurd : Type -> Type where
    MkAbsurd : Negation (Absurd a) -> Absurd a

but it's probably worth adding as a test case.

[dunhamsteve]

In case someone else needs it, the patch for LSP is fairly straightforward but can be found here: idris-community/idris2-lsp@main...dunhamsteve:idris2-lsp:update-for-3480

In addition to that change, it would also need the submodule updated to point at the latest Idris after this PR is merged.

[gallais]

Happy to merge. Should we get LSP up to speed first & merge on green?

[dunhamsteve]

I've put a pr in at idris-community/idris2-lsp#236

That should fix the tests and unblock pack, but idris2-lsp also has a submodule Idris2 that points to the revision that it works with. CI and pack ignore that submodule, but some users may may follow the instructions and use that. We can update that after the merge. Another option would be to point it directly to this PR.

[mattpolzin]

I can confirm the PR up for the LSP project builds against this branch of Idris2.

@dunhamsteve let's push a change to the Idris2 submodule in your LSP PR that points it at your branch so we can get that PR green in CI, merge it, and not have any commits of that project that don't build against the version of the compiler that the submodule points to.

Then, as you suggest, we can fast follow the merge of this Idris2 PR with another LSP PR that switches back to the upstream compiler at latest main.

[dunhamsteve]

@mattpolzin Sounds good, that PR is green now. I pushed this branch to idris-lang/Idris2, so LSP would still be pointing at the official idris repository.

[dunhamsteve]

I think pack is pinning the lsp to a specific commit, I didn't consider that bit.

[ build ] echo 'export idrisLSPVersion : ((Nat,Nat,Nat), String); idrisLSPVersion = ((0,1,0), "df322faeb")' >> src/Server/Generated.idr

I don't think we're going to get that test green before the merge. Pack is going to pin to the old idris2-lsp and the old idris until it sees idris2-lsp#main and idris2#main that work together.

[dunhamsteve]

Ok, I thought I saw a red build here, after the LSP merge, but it's green now.

[buzden]

I don't think we're going to get that test green before the merge. Pack is going to pin to the old idris2-lsp and the old idris until it sees idris2-lsp#main and idris2#main that work together.

If you are talking about idris2-lsp's CI, we can implement what we did for elab-utils: we run another CI job on the upstream's PR branch and all bleeding edge states of other libraries. The code is a bit clumsy and that's why I didn't suggest it anywhere, but if it's useful we still can do this

[mattpolzin]

If you are talking about idris2-lsp's CI, we can implement what we did for elab-utils: we run another CI job on the upstream's PR branch and all bleeding edge states of other libraries. The code is a bit clumsy and that's why I didn't suggest it anywhere, but if it's useful we still can do this

This setup wouldn't be as useful for the LSP repo because you can't point the LSP at bleeding edge of the compiler if you're trying to merge a change to the LSP before the matching compiler change has merged. The other reason it would be less of a good fit in that repo is because it is expected that the Idris2 submodule will build the LS at any given point in time so we generally want to update that submodule anyway and once you do that the LSP repo's CI will go green with its current setup.