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.

Sign up for GitHub

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

Jump to bottom

Evaluation of partial functions during conversion #3372

Open
zanzix opened this issue Aug 17, 2024 · 1 comment
Open

Evaluation of partial functions during conversion #3372

zanzix opened this issue Aug 17, 2024 · 1 comment
Labels
discussion: design implem: normalise

Comments

@zanzix
Copy link

zanzix commented Aug 17, 2024

I seem to have found a bug in how Idris evaluates case trees.

Steps to Reproduce

Take the code from here: https://gist.github.com/zanzix/d5e5642e4aef80bd02ccf5d97116f3b7
Uncomment out the line eval Set (MapFst t) = ?zzz

Expected Behavior

Idris evaluates the case tree

Observed Behavior

Idris hangs forever
@gallais
Copy link
Member

gallais commented Aug 18, 2024

You are explicitly trying to evaluate a partial function at the type level. It's bound to end badly.

EvalTy (ProdK k1 k2) p = (EvalTy k1 (Fst p), EvalTy k2 (Snd p))
EvalTy s (Fst {k1=s, k2} a) = fst (EvalTy (ProdK s k2) a)

Agda is careful to turn off unfolding of partial functions however I am not sure it would be
appropriate for Idris given its goal to be more fast-and-loose with these questions.

@gallais gallais changed the title Compiler hangs after looking at a case tree Evaluation of partial functions during conversion Aug 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
discussion: design implem: normalise
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gallais @zanzix