Idris2-boot
Idris2-boot copied to clipboard
case-split fails on private definition in nested namespace
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.