Compile dot patterns

[NathanielB123]

As of #439 it is actually correct behaviour for some clauses with dot patterns to get compiled to Haskell code (specifically when the argument is compiled to a term argument in Haskell - i.e. there is no dependent quantification).

Names given by the Agda programmer are retained where possible, but explicit dot patterns are just turned into wildcards

OLD:
Arguably it might be nice to retain names (e.g. prefixed by a _) when the dot pattern isn't provided explicitly, but this info does not appear to be retained by the time we reach internal syntax (I could certainly be missing something though)

[jespercockx]

Ah indeed, ideally Agda would keep track of the names of patterns corresponding to module parameters in the PatOrigin, but currently these just get assigned the Inserted origin. However, we do have the name still in compilePats but we drop it by applying namedArg to the pattern before calling compilePat. So we could get access to the name by making compilePat take a NamedArg DeBruijnPattern instead and then extracting the name from that.

[NathanielB123]

Yes good point - I did not look very carefully, my bad. The naming behaviour on this PR is now (as of the above commit):

• Dot pattern with no explicit name: becomes a wildcard _
• Dot pattern with explicit name/inferred dot pattern: _ prefixed to the given name
• Dot pattern from module param: module param name used

I like the idea of prefixing with _ if possible, so I think ideally dotted module parameters would also be named this way, but it is a bit awkward because the code that compiles module parameters currently does this entirely based off the type. Also there is the potential issue that the Agda programmer could prefix a different parameter name with an _, so modifying the names could then cause clashes, e.g.

checkSubst' : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) (ty : Bool) (rest : Telescope (x ∷ α) β) → @0 t ≡ ExtendTel ty rest → Bool
checkSubst' t _t rest refl = True

compiles to invalid Haskell

checkSubst' :: Telescope -> Bool -> Telescope -> Bool
checkSubst' _t _t rest = True

Because of this, I'm somewhat inclined to just use the names as-given (easier, and lower chance of weird edge cases)

[jespercockx]

After thinking about it for a bit I agree that prefixing names with _ is more hassle than it's worth. So the choice is between using the name of the argument or an underscore. I'm in favor of using the name as-is with one minor twist: we can use the name if the origin of the dot pattern is PatOSystem (which it will be for module parameters) but if the origin is anything else (e.g. PatODot) then the user wrote a manual dot pattern which we should either replace by an _ or flat-out reject (since dot patterns are not a Haskell concept), but not replace it with a variable name.

[NathanielB123]

I agree, but I think there is another case: the user wrote a variable, but this got elaborated into a dot pattern, e.g.:

checkSubst' : ∀ {@0 x α β} (t : Telescope α (x ∷ β)) (ty : Bool) (rest : Telescope (x ∷ α) β) → @0 t ≡ ExtendTel ty rest → Bool
checkSubst' t ty rest refl = True

For these, the origin is PatOVar, and we can conveniently get the name directly from that.

And actually, module parameters are compiled earlier (via compileModuleParams, which already has the correct behaviour - i.e. just creates a bunch of Hs.PVars) so I don't think we need to explicitly handle PatOSystem - unless there is some situation where module parameters can still sneak through?

[jespercockx]

I thought perhaps with your changes we would get rid of compileModuleParams completely and just compile them as regular function arguments for each clause, but if we keep that function then indeed what you're saying makes sense.

[jespercockx]

Please let me know if there are no further changes you want to make to this PR so I can merge it.

[NathanielB123]

Ah fair, yeah for now I don't think there is any need to remove compileModuleParams. I'm happy for this to be merged!