Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
MarcelineVQ opened this issue May 10, 2020 · 0 comments
Open

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

MarcelineVQ opened this issue May 10, 2020 · 0 comments
Labels
Confirmed bug Something isn't working

Comments

@MarcelineVQ
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Confirmed bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants