Refinement types plus Null/NonNull

[jamesmckinna]

EXPERIMENTAL/DRAFT: See #2092.

Refinement types, and their syntax, are (at present) neither here nor there, but the rest of the PR is a moderately extended exploration of one mode of use: defining the Refinement associated with being non-null for a 'typeclass' supporting a null/non-null field... including Nat, List, ...

Possible target(s):

• safe head function on `List'; UPDATED superseded/specialised by Add NonNull to Data.List.Relation.Unary.NonNull on the model of Data.Nat.Base.NonZero #2260 ?
• reimplement Data.List.NonEmpty?
• what else?

[jamesmckinna]

Fixed merge conflict, but the (previously committed) line about <-irrefl now seems orphaned out-of-place. Something to pursue in tidying up CHANGELOG for v2.0...

[gallais]

Are you aware of http://agda.github.io/agda-stdlib/Data.Refinement.html ?

[jamesmckinna]

Oh, for heaven's sake, RTFL...! 🤦
Thanks for the pointer. Sigh.

Still, what is there is fairly minimal, and few (none?) instantiations of the refinement concept elsewhere in the library, so should be room for ... refactoring, and reconciling the bool/Dec/Pred versions of the concept.

UPDATED: if #2260 is merged, then besides the wish for a conceptual reconciliation of all the Non* irrelevant instances as per issue #2092 , this could/should be closed as won't-merge or duplicate, while leaving the issue open...

[jamesmckinna]

I'm going to close this, in favour of #2260