How to user-define a type equality constraint?

[Anthony Clayden]

Type equality `(~)` is a fine constraint. It's mildly annoying I need
either `-XGADTs` or `-XTypeFamilies` to use it -- because I don't otherwise
need those extensions. OTOH it's not H2010 so it needs to be switched on
somehow.

I see the Committee is discussing what to do. It's to be enabled by
`-XTypeOperators`. That would be just as annoying for me -- I don't
otherwise use Type Operators. If TypeOperators is to be the default for
GHC2021, that more or less convinces me against GHC2021. (I'm not a
newbie/I want to fine-tune which extensions I'm using.)

@int-index says
https://mail.haskell.org/pipermail/ghc-steering-committee/2021-April/002373.html

> What convention do you have in mind? (~) is not that different from, say,
(+), which is a valid type operator:

I believe `(~)` is different in that I can't define it in user code(?)
Indeed:

> (~) is a special, magical constraint, like Coercible and Typeable. ...,
the idea is to (eventually) require an explicit import of
Data.Type.Equality to indicate the use of (~) in the code,

I'd be happy to not import `(~)`/not use TypeOperators, and define an
ordinary typeclass/constraint, say `TypeCast a b`. There's a `TypeCast`
defined in HList 2004, but it needs FunDeps; more awkwardly it needs a
method and for that method to appear in term-level code.

Can I user-define a conventional type-class that behaves more like `(~)`?

(The "convention I have in mind" is that already in H2010,`~` is a special
symbol for irrefutable patterns. Then I'd prefer constraint `(~)` is also
special syntax; and at term level I'd prefer it be available as a monadic
prefix operator.)

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20210402/90da05dc/attachment.html>