@@ -728,7 +728,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
728728 case M.lookup ctor (dataConstructors env) of
729729 Just (_, ty) -> do
730730 (_, fn) <- instantiatePolyTypeWithUnknowns (error "Data constructor types cannot contain constraints") ty
731− fn' <- replaceAllTypeSynonyms fn
731+ fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
732732 go binders fn'
733733 where
734734 go [] ty' = do
@@ -1005,7 +1005,9 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
10051005-- Check the type of a function application, rethrowing errors to provide a better error message
10061006--
10071007checkFunctionApplication :: Value -> Type -> Value -> Maybe Type -> UnifyT Type Check (Type, Value)
1008−checkFunctionApplication fn fnTy arg ret = rethrow (mkErrorStack errorMessage (Just (ValueError fn)) <>) $ checkFunctionApplication' fn fnTy arg ret
1008+checkFunctionApplication fn fnTy arg ret = rethrow (mkErrorStack errorMessage (Just (ValueError fn)) <>) $ do
1009+ subst <- unifyCurrentSubstitution <$> UnifyT get
1010+ checkFunctionApplication' fn (subst $? fnTy) arg (($?) subst <$> ret)
10091011 where
10101012 errorMessage = "Error applying function of type "
10111013 ++ prettyPrintType fnTy
@@ -1018,8 +1020,7 @@ checkFunctionApplication' :: Value -> Type -> Value -> Maybe Type -> UnifyT Type
10181020checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
10191021 tyFunction' =?= tyFunction
10201022 _ <- maybe (return Nothing) (subsumes Nothing retTy) ret
1021− subst <- unifyCurrentSubstitution <$> UnifyT get
1022− arg' <- check arg (subst $? argTy)
1023+ arg' <- check arg argTy
10231024 return (retTy, App fn arg')
10241025checkFunctionApplication' fn (ForAll ident ty _) arg ret = do
10251026 replaced <- replaceVarWithUnknown ident ty