On Tue, Jul 7, 2015 at 3:35 AM, Simon Peyton Jones
If you post a repro case someone (even me) might help. The devil is always in the details.
The smallest repro I can come up with (which is still related to the actual problem) is as follows. In case it matters for the solution, there are a number of important bits I've erased. Most importantly, the inferType function is actually mutually recursive with a checkType function, though that doesn't seem to be the cause of the problem. {-# LANGUAGE DataKinds, PolyKinds, GADTs #-} data Type = Fun Type Type data Sing :: Type -> * where SFun :: Sing i -> Sing j -> Sing (Fun i j) data AST :: (Type -> *) -> Type -> * where App :: ast (Fun a b) -> ast a -> AST ast b class ABT (abt :: Type -> *) where view :: abt a -> AST abt a unview :: AST abt a -> abt a class WellTypedABT (abt :: Type -> *) where unviewWT :: Sing a -> AST abt a -> abt a typeOf :: abt a -> Sing a data TypeCheckMonad a = TCM { unTCM :: a } instance Functor TypeCheckMonad where fmap f = TCM . f . unTCM instance Applicative TypeCheckMonad where pure = TCM TCM f <*> TCM x = TCM (f x) instance Monad TypeCheckMonad where return = pure TCM x >>= k = k x inferType :: (ABT abt, WellTypedABT abt') => abt a -> TypeCheckMonad (abt' a) inferType e0 = case view e0 of App e1 e2 -> do e1' <- inferType e1 case typeOf e1' of SFun typ2 typ3 -> do e2' <- inferType e2 return . unviewWT typ3 $ App e1' e2' -- Live well, ~wren