Nils Anders Danielsson
Nils Anders Danielsson
@AndrasKovacs [mentions](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#meta-freezing-and-approximate-occurs-checking) that smalltt can type-check something like the following code quickly: ```agda data _×_ (A B : Set₂) : Set₂ where _,_ : A → B → A ×...
One could perhaps get something working fairly quickly by taking the following approach: * When a meta-variable `α` is solved with `λ x̅.t`, instead of instantiating it directly, create a...
> Regarding performance, I strongly suspect that just disabling definitional singleton types by itself will not have a major impact on performance. The real impact would come from not having...
> A cubical `Sub A φ p` type can also be a definitional singleton, when `φ = i1`, with "center" `p 1=1`. We could disallow `BUILTIN SUB` if `--definitional-singletons` has...
> It involved adding an extra type argument to the occurs checker and some related functions, and reducing that type in appropriate places. One could imagine replacing the type by...
I [suggested](https://github.com/agda/agda/issues/4642#issuecomment-1513055271) two flags because the default could be "off" for record types with η-equality and erased fields (which have presumably not been used a lot yet), and "on" for...
> also disallow eta record types whose fields are all erased In a setting with linear types the following type is also potentially problematic: ```agda record R : Set where...
A possible problem with the alternative approach is that we might get code duplication, because we have two ways to represent top-level functions: either as regular functions, or as instantiated...
> One other way to handle generalized metas is to always instantiate metas if the solution is a variable or a metavariable. This would fire also in cases where the...
> > I suggested two flags because the default could be "off" for record types with η-equality and erased fields (which have presumably not been used a lot yet), and...