Nils Anders Danielsson

No, I have not used Stack.

``` $ stack --version | grep -v '^-' Version 2.5.1.1 i386 Compiled with: Warning: this is an unsupported build that may use different versions of dependencies and GHC than the...

``` $ stack upgrade --force-download Segmentation fault (core dumped) ```

I could build 57e31feb6a3b5622f3fce8f8022f058c03672688 using GHC 8.10.4. I'd like to test some of my code, but the standard library (https://github.com/agda/agda-stdlib/commit/d66a21f1242b893bb6ead4f6ef6da0a5490924c2) is not accepted by this version of Agda.

The following code is accepted by Agda 2.6.2-f9a1816, but rejected by 57e31feb6a3b5622f3fce8f8022f058c03672688: ```agda variable A B : Set P : A → Set x y : A _$_ : ((x...

> With heterogeneous unification, this instantiation is potentially unsound (as the types of the LHS and RHS do not match). > > A work around is to give the first...

> One possibility is to add a flag which, using the new constraint prioritization mechanism, will perform instantiations of metavariables which are only well-typed modulo as a last resort, and...

I tried to make one of my developments work with this branch (8fb611e). This failed, because Cubical Agda is not supported yet, but I made more than 20000 lines (`wc...

I think we should try to get this pull request into a state in which it can be merged before the code bit-rots too much. If I understand correctly the...

> @vlopezj, can you give us access to that code, and explain how it relates to the future-hetcon-no-compat branch? @vlopezj, did you see this?