I have the following code, and I would like this to fail type checking:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Control.Lens
data GADT e a where
One :: Greet e => String -> GADT e String
Two :: Increment e => Int -> GADT e Int
class Greet a where
_Greet :: Prism' a String
class Increment a where
_Increment :: Prism' a Int
instance Greet (Either String Int) where
_Greet = _Left
instance Increment (Either String Int) where
_Increment = _Right
run :: GADT e a -> Either String Int
run = go
where
go (One x) = review _Greet x
go (Two x) = review _Greet "Hello"
The idea is that each entry in the GADT has an associated error, which I'm modelling with a Prism
into some larger structure. When I "interpret" this GADT, I provide a concrete type for e
that has instances for all of these Prism
s. However, for each individual case, I don't want to be able to use instances that weren't declared in the constructor's associated context.
The above code should be an error, because when I pattern match on Two
I should learn that I can only use Increment e
, but I'm using Greet
. I can see why this works - Either String Int
has an instance for Greet
, so everything checks out.
I'm not sure what the best way to fix this is. Maybe I can use entailment from Data.Constraint
, or perhaps there's a trick with higher rank types.
Any ideas?
The problem is you're fixing the final result type, so the instance exists and the type checker can find it.
Try something like:
run :: GADT e a -> e
Now the result type can't pick the instance for review
and parametricity enforces your invariant.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With