Make Constraint and Type apart, in Core
I'm running into issues related to this and https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0032-constraint-vs-type.rst doesn't do it for me fully.
TL;DR My use case is kind of implementing something like TypeRep
, and I need to be able to tell Type
and Constraint
apart. I can now, because CONSTRAINT
and TYPE
are apart, but could not in GHC-9.4. I consider this to be lucky coincidence, but also wrong. TYPE
and CONSTRAINT
are apart, but TYPE LiftedRep
and CONSTRAINT LiftedRep
are not.
{-# LANGUAGE GHC2021, DataKinds, TypeFamilies #-}
import GHC.Exts
type family Equals a b where
Equals a a = True
Equals a b = False
type Ex1 = Equals TYPE CONSTRAINT
type Ex2 = Equals (TYPE LiftedRep) (CONSTRAINT LiftedRep)
{-
This is not right:
*Main> :kind! Ex1
Ex1 :: Bool
= False
*Main> :kind! Ex2
Ex2 :: Bool
= Equals (*) Constraint
-}
I think that Type
and Constraint
should be nominally distinct in Core, but could have the same representation, i.e. using casts to make types align, but make the abstraction zero cost.