Amélia

This is the typeclass we use for this in the 1Lab: ```agda record Funlike {ℓ ℓ' ℓ''} (A : Type ℓ) (arg : Type ℓ') (out : arg → Type...

Closing this since the implementation presented here would get rid of meta-solution uniqueness, and coming up with a correct solution is less "quick fix" and more "open research problem".

I permit the license of my contributions to the CC: Tweaked project to be changed to the Mozilla Public License, v. 2.0. Additionally, I assign copyright ownership of my project...

I have a `default.nix` that also pulls in `haskell-language-server`, which I prefer over `make typecheck` (though on memory constrained systems I would probably use `ghcid` instead). I switch between ```bash...

The local counterpart to this flag would be a pragma, attached to the definition of the "class", saying that it's *never* looked up in instance fields of visible/hidden arguments, only...

I really want this feature, but I'm still conflicted on whether a flag is the best solution. Off the top of my head, I can think of the following approaches:...

Getting rid of this behaviour is for sure the option I prefer, I just didn't want to propose breaking backwards compatibility because I'm annoyed at some notation :slightly_smiling_face: The question...

> We also know that the generalisation telescope meta will be solved later, it can't be blocked on the solution of an instance goal. @UlfNorell Actually, it _can_ depend on...

I believe the consensus we've reached is that the current behaviour (local, *non-instance* variables can introduce instances) will be off by default, and, when enabled, instance search will once again...

I don't mind either way since I don't use `make` — other than `succeed` and `fail`, with an `AGDA_BIN` set in `mk/config.mk`, built purely with `cabal`