BadUnification

module Test

public export
interface IxFunctor (f : (lbl : Type) -> (pre : List lbl) -> (post : List lbl) -> Type -> Type)
          where
  map : (a -> b) -> f ty pre post a -> f ty pre post b

public export
interface (IxFunctor f) =>
          IxApplicative (f : (lbl : Type) -> (pre : List lbl) -> (post : List lbl) -> Type -> Type)
          where
  pure  : {st : List lbl} -> a -> f lbl st st a
  (<*>) : f lbl pre inter (a -> b) -> f lbl inter post a -> f lbl pre post b


data Dummy : (lbl : Type) -> (pre, post : List lbl) -> Type -> Type where
  AmIDumb : a -> Dummy b pre post a


IxFunctor Dummy where
  map func (AmIDumb x) = AmIDumb (func x)

IxApplicative Dummy where
  pure x = ?pure_rhs
  (<*>) mf mx = ?app_rhs

{- Compilation error:

Test.idr:23:1--30:1:While processing right hand side of IxApplicative implementation at Test.idr:23:1--30:1 at Test.idr:23:1--30:1:
When unifying Dummy lbl post a inter and Dummy lbl inter post a
When unifying Dummy lbl st st a and Dummy lbl st a st
Mismatch between:
	st
and
	a

-}