`constructor`less records break soundness

[sjeulu]

Idris is able to fill in an impossible implicit argument if it's a constructorless record defined in another module.

Steps to Reproduce

module Broken

export
record VoidContainer where
  theVoid : Void

export
getVoid : (p : VoidContainer) => Void
getVoid {p} = p.theVoid

failing "Can't find an implementation for VoidContainer"
  a : 2 + 2 = 5
  a = absurd getVoid

module ADifferentOne

import Broken

a : 2 + 2 = 5
a = absurd getVoid

Expected Behavior

Idris shouldn't be able to infer a phantom VoidContainer in this case

Observed Behavior

But it is

[spcfox]

The reason is that the name of the generated constructor is MN: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Idris/Desugar.idr#L1302-L1306 so its definition is not stored in ttc: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Core/TTC.idr#L1106-L1109 https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Core/TTC.idr#L1120

Perhaps we should process MN in TTC. Another option is to generate UN as is done for interfaces: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Idris/Elab/Implementation.idr#L38-L42

[spcfox]

Another option is to generate UN as is done for interfaces:

This solves the problem with record but we can still get Void using elaborator script:

module Broken

import Language.Reflection

%default total

%language ElabReflection

decls : List Decl
decls =
  let con = MN "MkBroken" 0
   in [ IData EmptyFC (SpecifiedValue Export) Nothing $
              MkData EmptyFC `{ Broken } (Just `( Type )) []
                     [ MkTy EmptyFC (NoFC con) `( Void -> Broken ) ] ]

%runElab declare decls

module ProofOfFalse

import Broken

%default total

Uninhabited Broken

broken : Broken
broken = %search

void : Void
void = uninhabited broken

[dunhamsteve]

Idris probably shouldn't use things with erased types as solutions for autos.

It's interesting that the TTC.idr code suppresses those fields when isUserName (fullname gdef) || cwName (fullname gdef) but only reads them back in when isUserName name. I would expect those conditions to match.

If we don't want to make a username or serialize all of the MN / DN names, another option is to serialize everything if the def is a data constructor. (But that makes the condition more complicated.)

Auto only uses stuff in scope, should it be allowed to use hidden/unnamed record constructors?

[spcfox]

t's interesting that the TTC.idr code suppresses those fields when isUserName (fullname gdef) || cwName (fullname gdef) but only reads them back in when isUserName name. I would expect those conditions to match.

I was surprised, too. But, actually isUserName returns True for CaseBlock and WithBlock, so cwName is redundant https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Core/Name.idr#L118-L123

Auto only uses stuff in scope, should it be allowed to use hidden/unnamed record constructors?

I don't think there's anything wrong with using an unnamed constructor. Auto shouldn't use non-exported constructor, but we don't save visibility in ttc for MN

[spcfox]

I don't understand why we look at the name type. Judging from the message of this commit, this is done to avoid storing metavariable information. Wouldn't it be better to check the definition?

[dunhamsteve]

It looks like that change is trying to suppress the type information for metas. After they are solved, the definition is a PMDef, and I think they are indistinguishable from a user function (aside from having a MN name). And here we have something that is not a meta, but still has a machine name.

I printed the names that aren't loaded, and it looks like default implementations are the other case of a non-meta variable whose type is being erased: https://github.com/idris-lang/Idris2/blob/6c6ee58eb26dc6c9ca9897f6f079c3a4c0e9e8b7/src/Idris/Elab/Interface.idr#L426

I don't know if it matters that they don't have type information. (CaseName / WithName is not a problem because isUserName returns true for them.)

I think I would lean towards making the constructor name a UN unless we decide not to erase the types on those metas.

[spcfox]

I think we should handle any valid definition in TTImp, since we have an elaborator script. So we shouldn't focus on the name

[spcfox]

From my experiments, we can save all Defs except PMDef: https://github.com/spcfox/Idris2/commit/3ae04b5e2519e37dfc2aa9994cd14241ff7501de

Saving all PMDef breaks the frex tests. Maybe we should add a flag for PMDef that should not be saved? Again, I suggest not using name for this, because elaborator allows us to use any name constructor (except PV) anywhere.

Probably some other definitions shouldn't be saved, I'm just looking at the status of the tests.

[spcfox]

Also this bug can be reproduced without %search and data constructors:

module Broken

import Language.Reflection

%default total

%language ElabReflection

decls : List Decl
decls =
  let name = MN "broken" 0
   in [ IClaim $ NoFC $ MkIClaimData MW Private [] $ MkTy EmptyFC (NoFC name) `( Unit )
      , IDef EmptyFC name [PatClause EmptyFC (IVar EmptyFC name) `( MkUnit )] ]

%runElab declare decls

module Main

import Broken
import Language.Reflection

%default total

%language ElabReflection

void : Void
void = %runElab check $ IVar EmptyFC $ NS (MkNS ["Broken"]) $ MN "broken" 0

This passes typechecking because any type is converted to Erased. Maybe we should handle Erased more carefully when unifying? https://github.com/idris-lang/Idris2/blob/7481337b59682c91742ff7a287069275accd419a/src/Core/Normalise/Convert.idr#L432

[dunhamsteve]

Yeah, it seems problematic to me that Erased converts to anything. I tried changing the that line and the previous one to pure False (along with sticking True in for the save condition, so nothing is erased in TTC) and with a clean build Prelude.Interface fails to compile:

Error: While processing right hand side of Compose. Can't find an implementation for Functor (f . g).

So I guess we've got some erased/placeholder values floating around that are relied on. I do see an erased type on func in there, but I don't know if it's the root cause:

Main> :di Prelude.Interfaces.Functor.Compose
Prelude.Interfaces.Functor.Compose
Arguments [{arg:0}, {arg:1}, {arg:2}, {arg:3}]
Compile time tree: MkFunctor {f = (.) {a = Type} {c = Type} {b = Type} {arg:1} {arg:0}} (\0 b : Type,
0 a : Type,
func : ?_,
{arg:8945} : {arg:1} ({arg:0} a) => map {b} {a} {g = {arg:0}} {f = {arg:1}} {l = {arg:2}} {r = {arg:3}} func {arg:8945})

Other placeholders I see are types on all of the binders on metas, but I don't know if those are ever unified with anything. (It's interesting because I had trouble coming up with types in that situation in my own language because of interleaved lets and lambdas.)

I also couldn't sort out why frex was throwing AlreadyDefined in your other branch.