case-split fails on private definition in nested namespace

[edwinb]

Issue by MarcelineVQ
Sunday May 10, 2020 at 05:21 GMT
Originally opened as edwinb/Idris2-boot#363

---

Steps to Reproduce

module Main

namespace Foo1
  foo : Nat -> ()
  foo k1 = ?foo1_rhs
  
namespace Foo2
  export
  foo2 : Nat -> ()
  foo2 k2 = ?foo2_rhs

foo3 : Nat -> ()
foo3 k3 = ?foo3_rhs

Split k1 with any method, e.g. :cs 5 7 k1

Expected Behavior

Expect k1 k2 k3 can all be split to Z (S k) cases.

Observed Behavior

An error of No valid case splits but the underlying cause is a hidden error of :1:1--1:1:Name Main.Foo1.foo is private
This error comes from handleUnify in mkCase called from src/TTImp/Interactive/CaseSplit.idr:getSplitsLHS

This issue does not occur on private definitions that are at the top level, only in nested namespaces.
This issue also appears for the :gd command.

[jfdm]

I've recently been bitten by this bug, but have noticed an interesting aspect.

Given the following snippet:

module Bug

namespace BazzFoo
  public export
  data BazzFoo : Type where
    MkPair : Int -> BazzFoo

  getInt : BazzFoo -> Int
  getInt x = ?getInt_rhs

getInt : BazzFoo -> Int
getInt x = ?getInt_rhs_a

Case splitting on the pattern variable x in Bug.BazzFoo.getInt results in No valid case splits. However, case splitting on x in Bug.getInt works as expected.

[gallais]

Fixed by 72af040