Comments (3)
The problem is that with λ where
you don't necessarily get a simple list of all the fields: there can be other patterns or copatterns, and this can be different for each clause. To solve this properly, what we'd need to do is to first construct the case tree (inserting missing cases in the process) and only then check all of the right-hand sides. But this is not what we do currently: we start by typechecking each clause in isolation and only build the case tree after the fact. It's also not clear how we should deal with overlapping clauses if that strategy would be implemented.
from agda.
It's the same reason this also fails:
-- ✖ fails
_ : X
_ = λ where
.p → refl
.x → it
To type check the p
clause you need the x
clause to evaluate. Missing clauses are inserted after type checking the given clauses, so leaving it out behaves the same as writing it at the end.
I would be a little hesitant to say that we should postpone checking the p
clause until we know the value of the x
clause. You have to be very careful if doing that to not introduce cyclic dependencies between the clauses.
from agda.
OK, that makes some sense, it just didn't occur to me that the order of fields matters.
However, this still doesn't explain why the same thing using record
is not order-dependent; this seems somewhat inconsistent.
Also, shouldn't the type checker perform checks according to the dependency order of the fields (i.e. perform a topological sort first, then start type-checking individual fields) and whenever an instance field is encountered either search for a term given by the user, or otherwise appeal to instance resolution. Something like that..
from agda.
Related Issues (20)
- Mutually recursive definition doesn't recognize data constructor defined later HOT 4
- Mimer doesn't check existing constraints HOT 4
- Instance resolution runs too late, leads to `with`-abstraction failure HOT 18
- Test suite needs to be run with debug printing enabled HOT 1
- Internal error in Mimer with module parameter and matching
- Instance resolution failure in Agda 2.6.4 HOT 6
- Mimer drops part of the solution with module parameter
- Citation.cff HOT 1
- Prune the `Makefile` HOT 7
- Delete the GitHub Wiki HOT 3
- Migrate the Chalmers Wiki HOT 4
- Prune `Setup.hs` HOT 5
- Reorganize `HACKING.md`
- Merge `.authorspellings` and `.mailmap` HOT 1
- Mimer internal error when querying `recRecursive` HOT 1
- Interactive highlighting remnants with lambda-where
- Pattern synonyms with named arguments can be defined but not used HOT 3
- Automatically create names for syntax
- Mangled trX/Con clause for indexed type with green slime
- Why do we `reduce` and `instantiateFull` constraints? HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda.