How can I use restricted constraints with GADTs?

Question

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 Prisms. 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?

Answer 1

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.