search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
903 stars 58 forks source link

case-split fails on private definition in nested namespace #363

Open MarcelineVQ opened 4 years ago

MarcelineVQ commented 4 years ago

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.