Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

case-split fails on private definition in nested namespace

Open MarcelineVQ opened this issue 5 years ago • 0 comments

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.

MarcelineVQ avatar May 10 '20 05:05 MarcelineVQ