Consider the following code:
data T b where
T :: Maybe (a -> b) -> a -> T b
g (T (Just f) x) = f x
g (T Nothing x) = x
this does not compile, we get an error on the Nothing definition of g. The reason of this is because Nothing does not prevent the internal type a from being different to the externally visible type b.
Now consider this alternative approach:
data Maybe' b a where
Just' :: a -> Maybe' b a
Nothing' :: Maybe' b b
data T' b where
T' :: Maybe' (a -> a) (a -> b) -> a -> T' b
g' (T' (Just' f) x) = f x
g' (T' Nothing' x) = x
This compiles without issue.
Here's another fun example of what this allows:
dotMaybe ::
Maybe' (dummy1 -> dummy1) (b -> c) ->
Maybe' (dummy2 -> dummy2) (a -> b) ->
Maybe' (dummy2 -> dummy2) (a -> c)
dotMaybe (Just' f) (Just' g) = Just' (f . g)
dotMaybe (Just' f) Nothing' = Just' f
dotMaybe Nothing' (Just' g) = Just' g
dotMaybe Nothing' Nothing' = Nothing'
Is there a package already available on Hackage that allows for the sort of functionality demonstrated in Maybe', or should I package something up? I just don't want to reinvent the wheel.