How to user-define a type equality constraint?

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....
What convention do you have in mind? (~) is not that different from, say, (+), which is a valid type operator:
(~) is a special, magical constraint, like Coercible and Typeable. ...,
I believe `(~)` is different in that I can't define it in user code(?) Indeed: 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

On Apr 1, 2021, at 8:12 PM, Anthony Clayden
wrote: Can I user-define a conventional type-class that behaves more like `(~)`?
I don't think so. But why does this matter? I can't define `Char` in user code, but it's exported from the Prelude and requires no extensions. While I can define Eq in user code, I can't make `deriving` work with my version. I can't define `error` in user code. There are many others, I'm sure. So: why does this matter? Thanks, Richard

`Char` is defined in user code. What you really can't define are Char# and
TYPE, and you can't modify `RuntimeRep`. Speaking of `Char#`, I see that in
9.0, at least, it has kind TYPE 'WordRep. Why is that not Word32Rep?
On Mon, Apr 5, 2021, 10:50 PM Richard Eisenberg
On Apr 1, 2021, at 8:12 PM, Anthony Clayden
wrote: Can I user-define a conventional type-class that behaves more like `(~)`?
I don't think so.
But why does this matter? I can't define `Char` in user code, but it's exported from the Prelude and requires no extensions. While I can define Eq in user code, I can't make `deriving` work with my version. I can't define `error` in user code. There are many others, I'm sure.
So: why does this matter?
Thanks, Richard _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

That sounds like a bug/oversight! Is that not fixed in 9.2?
On Mon, Apr 5, 2021 at 11:08 PM David Feuer
`Char` is defined in user code. What you really can't define are Char# and TYPE, and you can't modify `RuntimeRep`. Speaking of `Char#`, I see that in 9.0, at least, it has kind TYPE 'WordRep. Why is that not Word32Rep?
On Mon, Apr 5, 2021, 10:50 PM Richard Eisenberg
wrote: On Apr 1, 2021, at 8:12 PM, Anthony Clayden
wrote: Can I user-define a conventional type-class that behaves more like `(~)`?
I don't think so.
But why does this matter? I can't define `Char` in user code, but it's exported from the Prelude and requires no extensions. While I can define Eq in user code, I can't make `deriving` work with my version. I can't define `error` in user code. There are many others, I'm sure.
So: why does this matter?
Thanks, Richard _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
participants (4)
-
Anthony Clayden
-
Carter Schonwald
-
David Feuer
-
Richard Eisenberg