blob: f1fd17ec8f001acea9a40ccc9ac20dd7e262462d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(..))
type family (x :: f a) <|> (y :: f a) :: f a
type family Mzero :: f a
monadPlusMplus :: forall f a (x :: f a) (y :: f a).
Proxy x -> Proxy y
-> Mzero x y :~: (x <|> y)
monadPlusMplus _ _ = _Refl
|
