Consider this somewhat silly datatype:
type data AllowPrimesOnly = PrimesOnly | AllNumbers
data Number (allowPrimesOnly :: AllowPrimesOnly) where
One :: Number AllNumbers
Two :: Number allowPrimesOnly
Three :: Number allowPrimesOnly
Four :: Number AllNumbers
Five :: Number allowPrimesOnly
With this definition, I can then define:
f :: Number allowPrimesOnly -> Int
f = \case
One -> 1
Two -> 2
Three -> 3
Four -> 4
Five -> 5
fPrime :: Number PrimesOnly -> Int
fPrime = \case
Two -> 2
Three -> 3
Five -> 5
quite happily, and GHC will give warnings (or no warnings) appropriately.
Note in particular with f
, it works with both types. Perhaps thereâs some inefficiencies applying f
to a Number PrimeOnly
because itâs checking branches that never exist but it still works.
But then when I try to do:
g :: Number PrimesOnly -> Number AllNumbers
g = coerce
I get a problem. I canât coerce
between different Number
types, because the role of allowPrimesOnly
is nominal
as Number
is a GADT.
Now lets say instead I define Number
like this:
data Number (allowPrimesOnly :: AllowPrimesOnly) = One | Two | Three | Four | Five
now:
g :: Number PrimesOnly -> Number AllNumbers
g = coerce
does work. But weâre now getting warnings for fPrime
. We can fix that though, with a bit of a hack:
view :: Number PrimesOnly -> Maybe Void
view = const Nothing
pattern MatchPrimesOnly :: Void -> Number PrimesOnly
pattern MatchPrimesOnly x <- (view -> Just x)
{-# COMPLETE Two, Three, Five, MatchPrimesOnly #-}
fPrime :: Number PrimesOnly -> Int
fPrime = \case
Two -> 2
Three -> 3
Five -> 5
MatchPrimesOnly x -> Void.absurd x
The MatchPrimesOnly
pattern is a bit of a hack to force the COMPLETE pragma to only apply to Number PrimesOnly
.
So far so good. Weâve got to add a bit of a hack to get the compiler to not warn when weâre only pattern matching against the primes (as just using a {-# COMPLETE Two, Three, Five #-}
would allow incomplete matches against Number AllNumbers
) but weâve got a problem now:
g2 :: Number AllNumbers -> Number PrimesOnly
g2 = coerce
works. And it shouldnât. Note we want the following:
thisShouldCompile :: Number PrimesOnly -> Number AllNumbers
thisShouldCompile = coerce
thisShouldCompileAsWell :: [Number PrimesOnly] -> [Number AllNumbers]
thisShouldCompileAsWell = coerce
butThisShouldFailToCompile :: Number AllNumbers -> Number PrimesOnly
butThisShouldFailToCompile = coerce
I donât just want to write:
doCoerce :: Number PrimesOnly -> Number AllNumbers
doCoerce = coerce
and expose it as a function, because then Iâll have to also write,
doCoerceHigher :: f (Number PrimesOnly) -> f (Number AllNumbers)
doCoerceHigher = coerce
Because I donât even know how to write this, and even this doesnât even cover all the possibilities where coerce
can be used.
Anyway to achieve what Iâm trying to achieve here?