Skip to content

Quantify the `a` in the `Functor (Either a)` instance

Ryan Scott requested to merge RyanGlScott/dependent:unsolved-meta-fix into main

Attempting to compile DH.Prelude with Agda 2.6.1.2 yields the following error:

$ agda DH/Prelude.agda
Checking DH.Prelude (/home/ryanglscott/Documents/Hacking/Agda/dependent/agda/DH/Prelude.agda).
Unsolved metas at the following locations:
  /home/ryanglscott/Documents/Hacking/Agda/dependent/agda/DH/Prelude.agda:451,35-36

I'm unclear if this is a leftover from development or just a newer version of Agda being stricter about quantification, but either way, the fix is simple.

Merge request reports