refactor: use a refinement type for Data.Vec

[4e554c4c]

resolves: #567

Description

As per a suggestion by @TOTBWF, this changes Data.Vec to use a refinement type which codes length xs = n.

Unfortunately this means that induction on vecs now needs vec-view, which makes some things messier. Worse still, I can't seem to use [] as a pattern for the empty vec since it conflicts with list, and use ∷ at all since it can't be a pattern.

The order of instances is also changed a little bit, which means [ p ] fails to realize as a list in 1Lab.Reflection.List.

I'd love some tips on how to make this a little bit cleaner :)

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

[Lavenza]

Pull request preview

Changed pages

• Data.Vec.Base (+94, -84)
• Data.Nat.Solver (+33, -27)
• Data.Vec.Properties (+26, -18)
• Meta.Idiom (+24, -14)
• Data.List.Base (+25, -8)
• Data.Maybe.Base (+18, -9)
• Realisability.Data.Nat (± 11)
• Realisability.Data.Sum (± 7)
• Realisability.PCA (+9, -5)
• Realisability.Data.Bool (± 6)
• Cat.Instances.Assemblies.Exponentials (± 5)
• Realisability.Data.Pair (± 5)

[4e554c4c]

this is now rebased on #597 and doesn't chmod borceaux

[4e554c4c]

rebase'd

[plt-amy]

i'm reading this on the github web editor so the line length limit comments are eyeballed