Andreas Abel
Andreas Abel
The `{-# OPTIONS -v tc.lhs.unify:30 #-}` diff of function argument vs. module parameter (extended lambda) is this: ```diff --- a/issue-8111-fun.txt +++ b/issue-8111-par.txt @@ -16,9 +16,9 @@ isEtaVar results: [Just 0,Just...
With verbosity 65 it becomes: ```diff @@ -11,24 +14,24 @@ initial unifyState: UnifyState equations: s =?= s₁ isEtaVar results: [Just 0,Just 1] fi = FlexibleVar {flexArgInfo = ArgInfo {argInfoHiding =...
The choice is made in `basicUnifyStrategy`: https://github.com/agda/agda/blob/3075bb09e50216f0dffdca0b9a067a20789c1acd/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs#L306-L335 However, it depends on the classification of flexible vars made earlier. It seems that the difference is just caused on the `Origin` of...
The termination checker has its own (more conservative) calculation of what is recursive and will mark recursive clauses as such. It does judge `[[_]]` as recursive, e.g. complains about `⟦...
> The core issue appears that we want primitive modules to be physical files (for inspection), so we need to place them somewhere. Yes. The current main question is if...
> I suppose I'll still work on reimplemnting it, Ah good! Yeah, let's have a proper implementation of it before we release it!
Updating for 2.8.0 RC2. Contains a revert of the fix of - #7876
Released
> Would it make sense to support this syntax instead? It should work if a case for `A.LetAxiom` is added; it would be basically identical to the `A.LetBind` case. Ah,...