hindley-milner-type-check 0.1.0.0 → 0.1.1.0

raw patch · 9 files changed

+491/−227 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• hindley-milner-type-check.cabal +4/−2
• src/Type/Check/HM/Infer.hs +178/−99
• src/Type/Check/HM/Lang.hs +5/−1
• src/Type/Check/HM/Pretty.hs +93/−51
• src/Type/Check/HM/Term.hs +37/−33
• src/Type/Check/HM/TyTerm.hs +9/−16
• src/Type/Check/HM/TypeError.hs +11/−2
• test/TM/NumLang.hs +153/−22
• test/TM/SKI.hs +1/−1

@@ -1,5 +1,5 @@ name:                   hindley-milner-type-check-version:                0.1.0.0+version:                0.1.1.0 synopsis:               Type inference for Hindley-Milner based languages description:     This package contains an implemention of Hindley-Milner inference algorithm.@@ -55,6 +55,7 @@   default-language:     Haskell2010    default-extensions:+    ConstraintKinds     DeriveDataTypeable     DeriveFunctor,     DeriveFoldable,@@ -73,9 +74,10 @@     TemplateHaskell,     TupleSections,     TypeFamilies,+    TypeApplications     TypeSynonymInstances -test-suite hindley-milner-tests+test-suite hindley-milner-type-check-tests   Type:                exitcode-stdio-1.0   Ghc-options:         -Wall -threaded -rtsopts   Default-Language:    Haskell2010

@@ -11,7 +11,7 @@ -- >   type Src  TestLang = ()              -- ^ define type for source code locations -- >   type Var  TestLang = Text            -- ^ define type for variables -- >   type Prim TestLang = NoPrim          -- ^ define type for primitive operators--- >   getPrimType _ = error "No primops"   -- ^ reports types for primitives+-- >   getPrimType _ _ = error "No primops"   -- ^ reports types for primitives -- -- Also we define context for type inference that holds types for all known variables -- Often it defines types for all global variables or functions that are external.@@ -40,17 +40,23 @@     Context(..)   , insertCtx   , lookupCtx+  , insertConstructorCtx+  , lookupConstructorCtx   , ContextOf   -- * Inference   , inferType   , inferTerm+  , inferTypeList+  , inferTermList   , subtypeOf   , unifyTypes   -- * Utils   , closeSignature+  , printInfer ) where  import Control.Monad.Identity+import Control.Monad.Writer.Strict  import Control.Applicative import Control.Arrow (second)@@ -69,29 +75,49 @@ import Type.Check.HM.Type import Type.Check.HM.TypeError import Type.Check.HM.TyTerm+import Type.Check.HM.Pretty  import qualified Data.Map.Strict as M import qualified Data.Set as S import qualified Data.List as L  -- | Context holds map of proven signatures for free variables in the expression.-newtype Context loc v = Context { unContext :: Map v (Signature loc v) }-  deriving (Show, Eq, Semigroup, Monoid)+data Context loc v = Context+  { context'binds         :: Map v (Signature loc v)   -- ^ known binds+  , context'constructors  :: Map v (Signature loc v)   -- ^ known constructors for user-defined types+  }+  deriving (Show, Eq) +instance Ord v => Semigroup (Context loc v) where+  (<>) (Context bs1 cs1) (Context bs2 cs2) = Context (bs1 <> bs2) (cs1 <> cs2)++instance Ord v => Monoid (Context loc v) where+  mempty = Context mempty mempty+ -- | Type synonym for context. type ContextOf q = Context (Src q) (Var q)  instance CanApply Context where-  apply subst = Context . fmap (apply subst) . unContext+  apply subst ctx = ctx+      { context'binds = fmap (apply subst) $ context'binds ctx+      }  -- | Insert signature into context insertCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v-insertCtx v sign (Context ctx) = Context $ M.insert v sign ctx+insertCtx v sign (Context binds cons) = Context (M.insert v sign binds) cons  -- | Lookup signature by name in the context of inferred terms. lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)-lookupCtx v (Context ctx) = M.lookup v ctx+lookupCtx v (Context binds _cons) = M.lookup v binds +-- | Insert signature into context+insertConstructorCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v+insertConstructorCtx v sign (Context binds cons) = Context binds (M.insert v sign cons)++-- | Lookup signature by name in the context of inferred terms.+lookupConstructorCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)+lookupConstructorCtx v (Context _binds cons) = M.lookup v cons+ -- | Wrapper with ability to generate fresh names data Name v   = Name v@@ -127,20 +153,24 @@ -- To check the term we need only variables that are free in the term. -- So we can safely remove everything else and speed up lookup times. restrictContext :: Ord v => Term prim loc v -> Context loc v -> Context loc v-restrictContext t (Context ctx) = Context $ M.intersection ctx fv+restrictContext t (Context binds cons) = Context (M.intersection binds fv) cons   where     fv = M.fromList $ fmap (, ()) $ S.toList $ freeVars t  wrapContextNames :: Ord v => Context loc v -> Context loc (Name v) wrapContextNames = fmapCtx Name   where-    fmapCtx f (Context m) = Context $ M.mapKeys f $ M.map (fmap f) m+    fmapCtx f (Context bs cs) = Context (wrap bs)  (wrap cs)+      where+        wrap = M.mapKeys f . M.map (fmap f)  wrapTermNames :: Term prim loc v -> Term prim loc (Name v) wrapTermNames = fmap Name  markProven :: Context loc v -> Context (Origin loc) v-markProven = Context . M.map (mapLoc Proven) . unContext+markProven (Context bs cs) = Context (mark bs) (mark cs)+  where+    mark = M.map (mapLoc Proven)  markUserCode :: Term prim loc v -> Term prim (Origin loc) v markUserCode = mapLoc UserCode@@ -180,33 +210,58 @@  -- | Type-inference monad. -- Contains integer counter for fresh variables and possibility to report type-errors.-newtype InferM loc var a = InferM (StateT Int (Except (TypeError loc (Name var))) a)-  deriving (Functor, Applicative, Monad, MonadState Int, MonadError (TypeError loc (Name var)))+newtype InferM loc var a = InferM (StateT Int (Writer [TypeError loc (Name var)]) a)+  deriving (Functor, Applicative, Monad, MonadState Int, MonadWriter [TypeError loc (Name var)])  -- | Runs inference monad.-runInferM :: InferM loc var a -> Either (TypeError loc (Name var)) a-runInferM (InferM m) = runExcept $ evalStateT m 0+runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a+runInferM (InferM m) = case runWriter $ evalStateT m 0 of+  (res, []) -> Right res+  (_, errs) -> Left errs  type InferOf q = InferM (Src q) (Var q) (Out (Prim q) (Src q) (Var q))  -- | Type-inference function. -- We provide a context of already proven type-signatures and term to infer the type.-inferType :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TypeOf q)+inferType :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TypeOf q) inferType ctx term = fmap termType $ inferTerm ctx term  -- | Infers types for all subexpressions of the given term. -- We provide a context of already proven type-signatures and term to infer the type.-inferTerm :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TyTermOf q)-inferTerm ctx term = join $-  bimap (fromTypeErrorNameVar . normaliseType) ((\(_, tyTerm) -> toTyTerm tyTerm)) $-    runInferM $ infer (wrapContextNames $ markProven $ restrictContext term ctx) (wrapTermNames $ markUserCode term)+inferTerm :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)+inferTerm ctx term =+  case runInferM $ infer (wrapContextNames $ markProven $ restrictContext term ctx) (wrapTermNames $ markUserCode term) of+    Right (_, tyTerm) -> toTyTerm tyTerm+    Left errs -> Left $ fmap (fromTypeErrorNameVar . normaliseType) errs   where-    toTyTerm = fromTyTermNameVar . normaliseType . mapLoc fromOrigin+    toTyTerm = either (Left . pure) Right . fromTyTermNameVar . normaliseType . mapLoc fromOrigin  type Out prim loc var = ( Subst (Origin loc) (Name var)                         , TyTerm prim (Origin loc) (Name var)                         ) +-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.+inferTermList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]+inferTermList ctx defs = case defs of+  []  -> pure []+  d:_ ->+    let topLoc = bind'loc d+    in  fmap fromLetExpr $ inferTerm ctx (toLetExpr topLoc defs)+  where+    toLetExpr loc ds = letRecE loc (fmap toBind ds) (bottomE loc)++    fromLetExpr = \case+      (TyTerm (Fix (Ann _ (LetRec _ bs _)))) -> fmap fromBind bs+      _                                      -> error "Imposible happened. Found non let-rec expression"++    toBind = id+    fromBind = fmap TyTerm++-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.+-- It returns only top-level types for all terms.+inferTypeList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]+inferTypeList ctx defs = fmap (fmap (fmap termType)) $ inferTermList ctx defs+ infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q infer ctx (Term (Fix x)) = case x of   Var loc v           -> inferVar ctx loc v@@ -216,14 +271,19 @@   Let loc v a         -> inferLet ctx loc (fmap Term v) (Term a)   LetRec loc vs a     -> inferLetRec ctx loc (fmap (fmap Term) vs) (Term a)   AssertType loc a ty -> inferAssertType ctx loc (Term a) ty-  Constr loc ty tag   -> inferConstr loc ty tag+  Constr loc tag      -> inferConstr ctx loc tag   Case loc e alts     -> inferCase ctx loc (Term e) (fmap (fmap Term) alts)   Bottom loc          -> inferBottom loc +retryWithBottom :: Lang q => TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q+retryWithBottom err loc = do+  tell [err]+  inferBottom loc+ inferVar :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q inferVar ctx loc v = {- trace (unlines ["VAR", ppShow ctx, ppShow v]) $ -}-  case M.lookup v (unContext ctx) of-    Nothing  -> throwError $ NotInScopeErr (fromOrigin loc) v+  case lookupCtx v ctx of+    Nothing  -> retryWithBottom (NotInScopeErr (fromOrigin loc) v) loc     Just sig -> do ty <- newInstance $ setLoc loc sig                    return (mempty, tyVarE ty loc v) @@ -231,17 +291,19 @@ inferPrim loc prim =   return (mempty, tyPrimE ty loc prim)   where-    ty = fmap Name $ mapLoc UserCode $ getPrimType prim+    ty = fmap Name $ mapLoc UserCode $ getPrimType (fromOrigin loc) prim  inferApp :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q inferApp ctx loc f a = {- fmap (\res -> trace (unlines ["APP", ppCtx ctx, ppShow' f, ppShow' a, ppShow' $ snd res]) res) $-} do   tvn <- fmap (varT loc) $ freshVar   res <- inferTerms ctx [f, a]   case res of-    (phi, [(tf, f'), (ta, a')]) -> fmap (\subst ->-                                            let ty   = apply subst tvn-                                                term = tyAppE ty loc (apply subst f') (apply subst a')-                                            in  (subst, term)) $ unify phi tf (arrowT loc ta tvn)+    (phi, [(tf, f'), (ta, a')]) -> case unify phi tf (arrowT loc ta tvn) of+      Left err    -> retryWithBottom err loc+      Right subst -> let ty   = apply subst tvn+                         term = tyAppE ty loc (apply subst f') (apply subst a')+                     in  pure (subst, term)+     _               -> error "Impossible has happened!"  inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q@@ -270,10 +332,11 @@   -> InferOf q inferLetRec ctx topLoc vs body = do   lhsCtx <- getTypesLhs vs-  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx)) exprBinds+  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx) mempty) exprBinds   let (tBinds, bindsTyTerms) = unzip rhsTyTerms-  (ctx1, lhsCtx1, subst) <- unifyRhs ctx lhsCtx phi tBinds-  inferBody bindsTyTerms ctx1 lhsCtx1 subst body+  case unifyRhs ctx lhsCtx phi tBinds of+    Right (ctx1, lhsCtx1, subst) -> inferBody bindsTyTerms ctx1 lhsCtx1 subst body+    Left err                     -> retryWithBottom err topLoc   where     exprBinds = fmap bind'rhs vs     locBinds  = fmap bind'loc vs@@ -303,60 +366,75 @@ inferAssertType :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q inferAssertType ctx loc a ty = do   (phi, aTyTerm) <- infer ctx a-  subst <- genSubtypeOf phi ty (termType aTyTerm)-  let subst' = phi <> subst-  return (subst', apply subst' $ tyAssertTypeE loc aTyTerm ty)+  case genSubtypeOf phi ty (termType aTyTerm) of+    Right subst -> do+      let subst' = phi <> subst+      return (subst', apply subst' $ tyAssertTypeE loc aTyTerm ty)+    Left err -> retryWithBottom err loc -inferConstr :: Lang q => Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q-inferConstr loc ty tag = do-  vT <- newInstance $ typeToSignature ty-  return (mempty, tyConstrE loc vT tag)+inferConstr :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q+inferConstr ctx loc tag = do+  case lookupConstructorCtx tag ctx of+    Just ty -> do+      vT <- newInstance ty+      return (mempty, tyConstrE loc vT tag)+    Nothing -> retryWithBottom (NotInScopeErr (fromOrigin loc) tag) loc  inferCase :: forall q . Lang q   => ContextOf' q -> Origin (Src q) -> TermOf' q -> [CaseAltOf' q (TermOf' q)]   -> InferOf q inferCase ctx loc e caseAlts = do   (phi, tyTermE) <- infer ctx e-  (psi, tRes, tyAlts) <- inferAlts phi (termType tyTermE) $ caseAlts-  return ( psi-         , apply psi $ tyCaseE tRes loc (apply psi tyTermE) $ fmap (applyAlt psi) tyAlts)+  mAlts <- inferAlts phi (termType tyTermE) $ caseAlts+  case mAlts of+    Just (psi, tRes, tyAlts) -> return ( psi+                                       , apply psi $ tyCaseE tRes loc (apply psi tyTermE) tyAlts)+    Nothing -> retryWithBottom (EmptyCaseExpr (fromOrigin loc)) loc   where-    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)])-    inferAlts substE tE alts =-      fmap (\(subst, _, tRes, as) -> (subst, tRes, L.reverse as)) $ foldM go (substE, tE, tE, []) alts+    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)]))+    inferAlts substE tE alts = do+      (subst, _, mTRes, as) <- foldM go (substE, tE, Nothing, []) alts+      pure $ case mTRes of+        Just tRes -> Just (subst, tRes, L.reverse as)+        Nothing   -> Nothing       where-        go (subst, tyTop, _, res) alt = do-          (phi, tRes, alt1) <- inferAlt (applyAlt subst alt)-          let subst1 = subst <> phi-          subst2 <- unify subst1 (apply subst1 tyTop) (apply subst1 $ caseAlt'constrType alt1)-          return (subst2, apply subst2 tyTop, apply subst2 tRes, applyAlt subst2 alt1 : res)---    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q))-    inferAlt preAlt = do-      alt <- newCaseAltInstance preAlt-      let argVars = fmap  (\ty -> (snd $ typed'value ty, (fst $ typed'value ty, typed'type ty))) $ caseAlt'args alt-          ctx1 = Context (M.fromList $ fmap (second $ monoT . snd) argVars) <> ctx-      (subst, tyTermRhs) <- infer ctx1 $ caseAlt'rhs alt-      let args = fmap (\(v, (argLoc, tv)) -> Typed (apply subst tv) (argLoc, v)) argVars-          alt' = alt-                  { caseAlt'rhs = tyTermRhs-                  , caseAlt'args = args-                  , caseAlt'constrType = apply subst $ caseAlt'constrType alt-                  }-      return (subst, termType tyTermRhs, alt')--    newCaseAltInstance :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))-    newCaseAltInstance alt = do-      tv <- newInstance $ typeToSignature $ getCaseType alt-      let (argsT, resT)= splitFunT tv-      return $ alt-        { caseAlt'constrType = resT-        , caseAlt'args = zipWith (\aT ty -> ty { typed'type = aT }) argsT $ caseAlt'args alt-        }+        go initSt@(subst, tyTop, mTyPrevRhs, res) alt = do+          mRes <- inferAlt (applyAlt subst alt)+          case mRes of+            Just (phi, tyRhs, tResExpected, alt1) -> do+              let subst1 = subst <> phi+              case unify subst1 (apply subst1 tyTop) (apply subst1 tResExpected) of+                Right subst2 -> do+                  case mTyPrevRhs of+                    Nothing -> pure (subst2, apply subst2 tyTop, Just $ apply subst2 tyRhs, applyAlt subst2 alt1 : res)+                    Just tyPrevRhs -> do+                      case unify subst2 (apply subst2 tyRhs) (apply subst2 tyPrevRhs) of+                        Right subst3 -> pure (subst3, apply subst3 tyTop, Just $ apply subst3 tyRhs, applyAlt subst3 alt1 : res)+                        Left err     -> do+                          tell [err]+                          pure initSt+                Left err     -> do+                  tell [err]+                  pure initSt+            Nothing -> do+              tell [NotInScopeErr (fromOrigin $ caseAlt'loc alt) (caseAlt'tag alt)]+              pure initSt -    getCaseType :: CaseAltOf' q (TermOf' q) -> TypeOf' q-    getCaseType CaseAlt{..} = funT (fmap typed'type caseAlt'args) caseAlt'constrType+    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q)))+    inferAlt alt =+      case lookupConstructorCtx (caseAlt'tag alt) ctx of+        Just ctxConTy -> do+          conTy <- newInstance ctxConTy+          let (tyArgs, tyRes) = splitFunT conTy+              expectedArity = length tyArgs+              actualArity   = length $ caseAlt'args alt+          when (expectedArity /= actualArity) $ tell [ConsArityMismatch (fromOrigin $ caseAlt'loc alt) (caseAlt'tag alt) expectedArity actualArity]+          let argVars = zipWith (\ty (src, arg) -> (arg, (src, ty))) tyArgs (caseAlt'args alt)+              ctx1 = Context (M.fromList $ fmap (second $ monoT . snd) argVars) mempty <> ctx+          (subst, tyTermRhs) <- infer ctx1 $ caseAlt'rhs alt+          let alt' = alt { caseAlt'rhs = tyTermRhs }+          return $ Just (subst, termType tyTermRhs, tyRes, alt')+        Nothing -> pure Nothing      splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)     splitFunT arrT = go [] arrT@@ -365,18 +443,9 @@           ArrowT _loc a b -> go (Type a : argsT) (Type b)           other           -> (reverse argsT, Type $ Fix other) +    applyAlt subst alt = alt { caseAlt'rhs = apply subst $ caseAlt'rhs alt } -    funT :: [TypeOf' q] -> TypeOf' q -> TypeOf' q-    funT argsT resT = foldr (\a b -> arrowT (getLoc a) a b) resT argsT -    applyAlt subst alt@CaseAlt{..} = alt-      { caseAlt'constrType = apply subst caseAlt'constrType-      , caseAlt'args       = fmap applyTyped caseAlt'args-      , caseAlt'rhs        = apply subst caseAlt'rhs-      }-      where-        applyTyped ty@Typed{..} = ty { typed'type = apply subst $ typed'type }- inferBottom :: Lang q => Origin (Src q) -> InferOf q inferBottom loc = do   ty <- fmap (varT loc) freshVar@@ -414,11 +483,11 @@  -- | Unification function. Checks weather two types unify. -- First argument is current substitution.-unify :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+unify :: (IsVar v, Show loc)   => Subst' loc v   -> Type' loc v   -> Type' loc v-  -> m (Subst' loc v)+  -> Either (TypeError loc (Name v)) (Subst' loc v) unify phi (Type (Fix x)) (Type (Fix y)) = {- trace (unlines ["UNIFY", ppShow tx, ppShow ty]) $ -}   case (x, y) of     (VarT loc tvn, t) ->@@ -459,11 +528,11 @@   | memberVarSet tvn (tyVars ty)  = throwError $ OccursErr (fromOrigin loc) (mapLoc fromOrigin ty)   | otherwise                     = return $ phi <> delta tvn ty -unifyl :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+unifyl :: (IsVar v, Show loc)   => Subst' loc v   -> [Type' loc v]   -> [Type' loc v]-  -> m (Subst' loc v)+  -> Either (TypeError loc (Name v)) (Subst' loc v) unifyl subst as bs = foldr go (return subst) $ zip as bs   where     go (a, b) eSubst = (\t -> unify t a b) =<< eSubst@@ -475,11 +544,11 @@   join $ bimap (fromTypeErrorNameVar . normaliseType) (fromSubstNameVar . fromSubstOrigin) $     genSubtypeOf mempty (fmap Name $ mapLoc Proven a) (fmap Name $ mapLoc UserCode b) -genSubtypeOf :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+genSubtypeOf :: (IsVar v, Show loc)   => Subst' loc v   -> Type' loc v   -> Type' loc v-  -> m (Subst' loc v)+  -> Either (TypeError loc (Name v)) (Subst' loc v) genSubtypeOf phi tx@(Type (Fix x)) ty@(Type (Fix y)) = case (x, y) of   (_, VarT _ _) -> unify phi tx ty   (ConT locA n xs, ConT locB m ys) ->@@ -498,11 +567,11 @@     subtypeErr locA locB = throwError       $ SubtypeErr (chooseUserOrigin locA locB) (mapLoc fromOrigin tx) (mapLoc fromOrigin ty) -subtypeOfL :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+subtypeOfL :: (IsVar v, Show loc)   => Subst' loc v   -> [Type' loc v]   -> [Type' loc v]-  -> m (Subst' loc v)+  -> Either (TypeError loc (Name v)) (Subst' loc v) subtypeOfL subst as bs = foldr go (return subst) $ zip as bs   where     go (a, b) eSubst = (\t -> genSubtypeOf t a b) =<< eSubst@@ -514,7 +583,7 @@ addDecls vs ctx =   foldM  (\c b -> addDecl unknowns b c) ctx vs   where-    unknowns = foldMap tyVars $ unContext ctx+    unknowns = foldMap tyVars $ context'binds ctx  addDecl :: forall loc v . IsVar v   => VarSet' loc v@@ -523,7 +592,8 @@   -> InferM loc v (Context' loc v) addDecl unknowns b ctx = do   scheme <- toScheme unknowns (bind'rhs b)-  return $ Context . M.insert (bind'lhs b) scheme . unContext $ ctx+  return $ ctx+    { context'binds = M.insert (bind'lhs b) scheme . context'binds $ ctx }   where     toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)     toScheme uVars ty = do@@ -566,6 +636,7 @@     SubtypeErr loc tA tB -> liftA2 (SubtypeErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)     NotInScopeErr loc v  -> fmap (NotInScopeErr loc) $ fromNameVar v     EmptyCaseExpr loc    -> pure $ EmptyCaseExpr loc+    ConsArityMismatch loc v expected actual -> fmap (\x -> ConsArityMismatch loc x expected actual) (fromNameVar v)     FreshNameFound       -> pure FreshNameFound  fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)@@ -590,19 +661,18 @@       Let loc bind a      -> fmap (\b -> Let loc b a) $ fromBind bind       LetRec loc binds a  -> fmap (\bs -> LetRec loc bs a) $ mapM fromBind binds       AssertType loc a ty -> fmap (AssertType loc a) $ fromTypeNameVar ty-      Constr loc t v      -> liftA2 (Constr loc) (fromTypeNameVar t) (fromNameVar v)+      Constr loc v        -> fmap (Constr loc) (fromNameVar v)       Bottom loc          -> pure $ Bottom loc       Case loc e alts     -> fmap (Case loc e) $ mapM fromAlt alts      fromBind b = fmap (\a -> b { bind'lhs = a }) $ fromNameVar $ bind'lhs b      fromAlt alt@CaseAlt{..} =-      liftA3 (\tag args constrType -> alt { caseAlt'tag = tag, caseAlt'args = args, caseAlt'constrType = constrType })+      liftA2 (\tag args -> alt { caseAlt'tag = tag, caseAlt'args = args })         (fromNameVar caseAlt'tag)-        (mapM fromTyped caseAlt'args)-        (fromTypeNameVar caseAlt'constrType)+        (mapM fromAltArg caseAlt'args) -    fromTyped Typed{..} = liftA2 Typed (fromTypeNameVar typed'type) (mapM fromNameVar typed'value)+    fromAltArg (loc, v) = fmap (loc , ) (fromNameVar v)  fromSubstNameVar :: Ord v => Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v) fromSubstNameVar (Subst m) = fmap (Subst . M.fromList) $ mapM uncover $ M.toList m@@ -617,4 +687,13 @@ closeSignature argTys sig = apply (Subst $ M.fromList $ zip argNames argTys) monoTy   where     (argNames, monoTy) = splitSignature sig++----------------------------------------------------------------------------------++-- | Pretty printer for result of type-inference+printInfer :: (PrettyLang q) => (Either [ErrorOf q] (TypeOf q)) -> IO ()+printInfer = \case+  Right ty  -> putStrLn $ show $ pretty ty+  Left errs -> mapM_ (putStrLn . (++ "\n") . show . pretty) errs+ 

@@ -8,8 +8,10 @@   , TyTermOf   , SubstOf   , ErrorOf+  , PrettyLang ) where +import Type.Check.HM.Pretty import Type.Check.HM.Term import Type.Check.HM.Subst import Type.Check.HM.Type@@ -48,7 +50,7 @@   type Prim q    -- | Reports type for primitive.-  getPrimType :: Prim q -> TypeOf q+  getPrimType :: Src q -> Prim q -> TypeOf q  -- | Types of our language type TypeOf q = Type (Src q) (Var q)@@ -64,5 +66,7 @@  -- | Type substitutions type SubstOf q = Subst (Src q) (Var q)++type PrettyLang q = (Lang q, PrettyVar (Var q), Pretty (Src q))  

@@ -1,10 +1,12 @@ {-# OPTIONS_GHC -Wno-orphans #-} -- | Pretty printer for types and terms. module Type.Check.HM.Pretty(-    HasPrefix(..)+    PrettyVar+  , FixityCtx(..)   , PrintCons(..)   , OpFix(..)   , Fixity(..)+  , Pretty(..) ) where  import Data.Bool@@ -15,101 +17,116 @@  import Type.Check.HM.Type import Type.Check.HM.Term---- | Class to querry fixity of infix operations.-class IsVar v => HasPrefix v where-  getFixity :: v -> Maybe OpFix--instance HasPrefix Text where-  getFixity = const Nothing+import Type.Check.HM.TypeError -instance HasPrefix String where-  getFixity = const Nothing+-- | Type to querry fixity of infix operations in type variables.+data FixityCtx var a = FixityCtx+  { fixity'context :: var -> Maybe OpFix   -- ^ Function that provides fixity-type for a given variable+  , fixity'data    :: a                    -- ^ content+  } -instance HasPrefix Int where-  getFixity = const Nothing+-- | Ignores fixity information+noFixity :: forall v a . a -> FixityCtx v a+noFixity = FixityCtx (const Nothing)  -- | This class is useful to define the way to print special cases -- like constructors for tuples or lists. class PrintCons v where   printCons :: v -> [Doc ann] -> Doc ann +instance PrintCons Int where+  printCons name args = hsep $ pretty name : args++instance PrintCons String where+  printCons name args = hsep $ pretty name : args+ instance PrintCons Text where   printCons name args = hsep $ pretty name : args -isPrefix :: HasPrefix v => v -> Bool-isPrefix = isNothing . getFixity+isPrefix :: (v -> Maybe OpFix) -> v -> Bool+isPrefix getFixity = isNothing . getFixity -isInfix :: HasPrefix v => v -> Bool-isInfix  = not . isPrefix+isInfix :: (v -> Maybe OpFix) -> v -> Bool+isInfix a = not . isPrefix a -instance (Pretty v, PrintCons v, HasPrefix v) => Pretty (Signature loc v) where-  pretty = foldFix go . unSignature+type PrettyVar a = (Pretty a, PrintCons a, IsVar a)++instance (PrettyVar v) => Pretty (Signature loc v) where+  pretty = pretty . noFixity @v++instance (PrettyVar v) => Pretty (FixityCtx v (Signature loc v)) where+  pretty (FixityCtx getFixity sign) = foldFix go $ unSignature sign     where       go = \case         ForAllT _ _ r -> r-        MonoT ty      -> pretty ty+        MonoT ty      -> pretty (FixityCtx getFixity ty) -instance (HasPrefix v, PrintCons v, Pretty v) => Pretty (Type loc v) where-  pretty = go False initCtx . unType+instance (PrettyVar v) => Pretty (Type loc v) where+  pretty = pretty . noFixity @v++instance (PrettyVar v) => Pretty (FixityCtx v (Type loc v)) where+  pretty (FixityCtx getFixity ty) = go False initCtx $ unType ty     where       go :: Bool -> FixityContext v -> Fix (TypeF loc v) -> Doc ann       go isArrPrev ctx (Fix expr) = case expr of         VarT _ name   -> pretty name-        ConT _ name [a, b] | isInfix name -> fromBin name a b+        ConT _ name [a, b] | isInfix getFixity name -> fromBin name a b         ConT _ name as -> fromCon isArrPrev name as         ArrowT _ a b -> fromArrow a b         TupleT _ as -> fromTuple as         ListT _ a -> fromList a         where-          fromCon isArr name args = maybeParens (not (null args) && not isArr && needsParens ctx OpFunAp) $+          fromCon isArr name args = maybeParens (not (null args) && not isArr && needsParens getFixity ctx OpFunAp) $             printCons name $ fmap (go False (FcRight OpFunAp)) args -          fromBin op a b = maybeParens (needsParens ctx (Op op)) $ hsep+          fromBin op a b = maybeParens (needsParens getFixity ctx (Op op)) $ hsep             [ go True (FcLeft $ Op op) a             , pretty op             , go True (FcRight $ Op op) b             ] -          fromArrow a b = maybeParens (needsParens ctx ArrowOp) $ hsep+          fromArrow a b = maybeParens (needsParens getFixity ctx ArrowOp) $ hsep             [ go True (FcLeft ArrowOp ) a             , "->"             , go True (FcRight ArrowOp) b             ] -          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . Type) as+          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . FixityCtx getFixity . Type) as -          fromList a = brackets $ pretty $ Type a+          fromList a = brackets $ pretty $ FixityCtx getFixity $ Type a        initCtx = FcNone  maybeParens :: Bool -> Doc ann -> Doc ann maybeParens cond = bool id parens cond -needsParens :: HasPrefix v => FixityContext v -> Operator v -> Bool-needsParens = \case+needsParens :: (v -> Maybe OpFix) -> FixityContext v -> Operator v -> Bool+needsParens getFixity = \case   FcNone      -> const False   FcLeft ctx  -> fcLeft ctx   FcRight ctx -> fcRight ctx   where     fcLeft ctxt op-      | comparePrec ctxt op == PoLT = False-      | comparePrec ctxt op == PoGT = True-      | comparePrec ctxt op == PoNC = True+      | comparePrec' ctxt op == PoLT = False+      | comparePrec' ctxt op == PoGT = True+      | comparePrec' ctxt op == PoNC = True       -- otherwise the two operators have the same precedence-      | fixity ctxt /= fixity op = True-      | fixity ctxt == FixLeft = False+      | fixity' ctxt /= fixity' op = True+      | fixity' ctxt == FixLeft = False       | otherwise = True      fcRight ctxt op-      | comparePrec ctxt op == PoLT = False-      | comparePrec ctxt op == PoGT = True-      | comparePrec ctxt op == PoNC = True+      | comparePrec' ctxt op == PoLT = False+      | comparePrec' ctxt op == PoGT = True+      | comparePrec' ctxt op == PoNC = True       -- otherwise the two operators have the same precedence-      | fixity ctxt /= fixity op = True-      | fixity ctxt == FixRight = False+      | fixity' ctxt /= fixity' op = True+      | fixity' ctxt == FixRight = False       | otherwise = True +    comparePrec' = comparePrec getFixity+    fixity' = fixity getFixity+ data PartialOrdering = PoLT | PoGT | PoEQ | PoNC   deriving Eq @@ -136,14 +153,14 @@   [ (Op "->", OpFix FixRight 2) ] -} -getFixityEnv :: HasPrefix v => Operator v -> Maybe OpFix-getFixityEnv = \case+getFixityEnv :: (v -> Maybe OpFix) -> Operator v -> Maybe OpFix+getFixityEnv getFixity = \case   OpFunAp -> Nothing   Op v    -> getFixity v   ArrowOp -> Just $ OpFix FixRight 2 -comparePrec :: HasPrefix v => Operator v -> Operator v -> PartialOrdering-comparePrec a b = case (getFixityEnv a, getFixityEnv b) of+comparePrec :: (v -> Maybe OpFix) -> Operator v -> Operator v -> PartialOrdering+comparePrec getFixity a b = case (getFixityEnv getFixity a, getFixityEnv getFixity b) of   (Just opA, Just opB) -> toPo (opFix'prec opA) (opFix'prec opB)   _                    -> PoNC   where@@ -153,13 +170,17 @@       | otherwise = PoEQ  -fixity :: HasPrefix v => Operator v -> Fixity-fixity op = maybe FixNone opFix'fixity $ getFixityEnv op+fixity :: (v -> Maybe OpFix) -> Operator v -> Fixity+fixity getFixity op = maybe FixNone opFix'fixity $ getFixityEnv getFixity op ----------------------------------------+-----------------------------------------------------------------+-- pretty terms -instance (HasPrefix v, PrintCons v, Pretty v, Pretty prim) => Pretty (Term prim loc v) where-  pretty (Term x) = foldFix prettyTermF x+instance (PrettyVar v, Pretty prim) => Pretty (Term prim loc v) where+  pretty = pretty . noFixity @v++instance (PrettyVar v, Pretty prim) => Pretty (FixityCtx v (Term prim loc v)) where+  pretty (FixityCtx getFixity (Term x)) = foldFix prettyTermF x     where       prettyTermF = \case         Var _ v            -> pretty v@@ -168,8 +189,8 @@         Lam _ v a          -> parens $ hsep [hcat ["\\", pretty v], "->", a]         Let _ v a          -> onLet [v] a         LetRec _ vs a      -> onLet vs a-        AssertType _ r sig -> parens $ hsep [r, "::", pretty sig]-        Constr _ _ tag     -> pretty tag+        AssertType _ r sig -> parens $ hsep [r, "::", pretty $ FixityCtx getFixity sig]+        Constr _ tag       -> pretty tag         Case _ e alts      -> vcat [ hsep ["case", e, "of"], indent 4 $ vcat $ fmap onAlt alts]         Bottom _           -> "_|_"         where@@ -178,7 +199,28 @@                  , hsep ["in ", body]]            onAlt CaseAlt{..} = hsep-            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd . typed'value) caseAlt'args+            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd) caseAlt'args             , "->"             , caseAlt'rhs ]++-----------------------------------------------------------------+-- pretty errors++instance (Pretty loc, PrettyVar var) => Pretty (TypeError loc var) where+  pretty = pretty . noFixity @var++instance (Pretty loc, PrettyVar var) => Pretty (FixityCtx var (TypeError loc var)) where+  pretty (FixityCtx getFixity tyErr) = case tyErr of+    OccursErr src name     -> err src $ hsep ["Occurs error", prettyTy name]+    UnifyErr src tyA tyB   -> err src $ hsep ["Type mismatch got", inTicks $ prettyTy tyB, "expected", inTicks $ prettyTy tyA]+    NotInScopeErr src name -> err src $ hsep ["Not in scope", pretty name]+    SubtypeErr src tyA tyB -> err src $ hsep ["Subtype error", inTicks $ prettyTy tyB, "expected", inTicks $ prettyTy tyA]+    EmptyCaseExpr src      -> err src $ "Case-expression should have at least one alternative case"+    FreshNameFound         -> "Impossible happened: failed to eliminate fresh name on type-checker stage"+    ConsArityMismatch src tag expected actual -> err src $ hsep ["Case-expression arguments mismatch for ", pretty tag, ". Expected ", pretty expected, " arguments, but got ", pretty actual]+    where+      err src msg = vcat [hcat [pretty src, ": error: "], indent 4 msg]+      inTicks x = hcat ["'", x, "'"]+      prettyTy = pretty . FixityCtx getFixity+ 

@@ -15,12 +15,15 @@   , constrE   , bottomE   , freeVars+  , sortDeps ) where  import Control.Arrow  import Data.Data+import Data.Graph import Data.Fix+import Data.Foldable import Data.Set (Set) import Data.Eq.Deriving import Data.Ord.Deriving@@ -30,6 +33,7 @@ import Type.Check.HM.Type  import qualified Data.Set as S+import qualified Data.Sequence as Seq  -- | Term functor. The arguments are -- @loc@ for source code locations, @v@ for variables, @r@ for recurion.@@ -42,8 +46,7 @@     | LetRec loc [Bind loc v r] r     -- ^ Recursive  let bindings     | AssertType loc r (Type loc v)   -- ^ Assert type.     | Case loc r [CaseAlt loc v r]    -- ^ case alternatives-    | Constr loc (Type loc v) v       -- ^ constructor with tag and arity, also we should provide the type-                                      --   of constructor as a function for a type-checker+    | Constr loc v                    -- ^ constructor with tag     | Bottom loc                      -- ^ value of any type that means failed program.     deriving (Show, Eq, Functor, Foldable, Traversable, Data) @@ -53,10 +56,8 @@   -- ^ source code location   , caseAlt'tag   :: v   -- ^ tag of the constructor-  , caseAlt'args  :: [Typed loc v (loc, v)]+  , caseAlt'args  :: [(loc, v)]   -- ^ arguments of the pattern matching-  , caseAlt'constrType :: Type loc v-  -- ^ type of the result expression, they should be the same for all cases   , caseAlt'rhs   :: a   -- ^ right-hand side of the case-alternative   }@@ -65,10 +66,10 @@ -- | Local variable definition. -- -- > let lhs = rhs in ...-data Bind loc var r = Bind+data Bind loc var a = Bind   { bind'loc :: loc             -- ^ Source code location   , bind'lhs :: var             -- ^ Variable name-  , bind'rhs :: r               -- ^ Definition (right-hand side)+  , bind'rhs :: a               -- ^ Definition (right-hand side)   } deriving (Show, Eq, Functor, Foldable, Traversable, Data)  $(deriveShow1 ''TermF)@@ -97,17 +98,14 @@         LetRec loc vs a -> Fix $ LetRec loc (fmap (\b ->  b { bind'lhs = f $ bind'lhs b }) vs) a         AssertType loc r sig -> Fix $ AssertType loc r (fmap f sig)         Case loc a alts -> Fix $ Case loc a $ fmap (mapAlt f) alts-        Constr loc ty v -> Fix $ Constr loc (fmap f ty) (f v)+        Constr loc v -> Fix $ Constr loc (f v)         Bottom loc -> Fix $ Bottom loc        mapAlt g alt@CaseAlt{..} = alt         { caseAlt'tag  = f caseAlt'tag-        , caseAlt'args = fmap (mapTyped g) caseAlt'args-        , caseAlt'constrType = fmap f caseAlt'constrType+        , caseAlt'args = fmap (second g) caseAlt'args         } -      mapTyped g Typed{..} = Typed (fmap f typed'type) (second g typed'value)- -- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@. varE :: loc -> var -> Term prim loc var varE loc = Term . Fix . Var loc@@ -142,8 +140,8 @@ caseE loc (Term e) alts = Term $ Fix $ Case loc e $ fmap (fmap unTerm) alts  -- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.-constrE :: loc -> Type loc v -> v -> Term prim loc v-constrE loc ty tag = Term $ Fix $ Constr loc ty tag+constrE :: loc -> v -> Term prim loc v+constrE loc tag = Term $ Fix $ Constr loc tag  -- | 'bottomE' @loc@ constructs bottom value. bottomE :: loc -> Term prim loc v@@ -162,7 +160,7 @@     Let loc _ _ -> loc     LetRec loc _ _ -> loc     AssertType loc _ _ -> loc-    Constr loc _ _ -> loc+    Constr loc _ -> loc     Case loc _ _ -> loc     Bottom loc -> loc @@ -177,20 +175,17 @@         Let loc v a  -> Fix $ Let (f loc) (v { bind'loc = f $ bind'loc v }) a         LetRec loc vs a -> Fix $ LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a         AssertType loc r sig -> Fix $ AssertType (f loc) r (mapLoc f sig)-        Constr loc ty v -> Fix $ Constr (f loc) (mapLoc f ty) v+        Constr loc v -> Fix $ Constr (f loc) v         Case loc e alts -> Fix $ Case (f loc) e (fmap mapAlt alts)         Bottom loc -> Fix $ Bottom (f loc)        mapAlt alt@CaseAlt{..} = alt         { caseAlt'loc  = f caseAlt'loc-        , caseAlt'args = fmap mapTyped caseAlt'args-        , caseAlt'constrType = mapLoc f caseAlt'constrType+        , caseAlt'args = fmap (first f) caseAlt'args         } -      mapTyped (Typed ty val) = Typed (mapLoc f ty) (first f val)- -- | Get free variables of the term.-freeVars :: Ord v => Term lprim oc v -> Set v+freeVars :: Ord v => Term prim loc v -> Set v freeVars = foldFix go . unTerm   where     go = \case@@ -205,28 +200,37 @@                              in  (mappend (freeBinds binds) body) `S.difference` lhs       AssertType _ a _    -> a       Case _ e alts       -> mappend e (foldMap freeVarAlts alts)-      Constr _ _ _        -> mempty+      Constr _ _          -> mempty       Bottom _            -> mempty      freeBinds = foldMap bind'rhs -    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap (snd . typed'value) caseAlt'args)+    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap snd caseAlt'args)  instance TypeFunctor (Term prim) where   mapType f (Term term) = Term $ foldFix go term     where       go = \case-        Constr loc ty cons       -> Fix $ Constr loc (f ty) cons-        Case loc e alts          -> Fix $ Case loc e $ fmap applyAlt alts-        other                    -> Fix other--      applyAlt alt@CaseAlt{..} = alt-        { caseAlt'args       = fmap applyTyped caseAlt'args-        , caseAlt'constrType = f caseAlt'constrType-        }--      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }+        AssertType loc r ty  -> Fix $ AssertType loc r (f ty)+        other                 -> Fix other  instance CanApply (Term prim) where   apply subst term = mapType (apply subst) term++-------------------------------------------------------------------------+-- sort terms by dependency order (it ignores cyclic depepndencies)++sortDeps :: Ord v => [(v, Term prim loc v)] -> [(v, Term prim loc v)]+sortDeps = fromDepGraph . stronglyConnComp . toDepGraph+  where+    toDepGraph = fmap (\(name, term) -> ((name, term), name, S.toList $ freeVars term))++    fromDepGraph = toList . foldMap getVertex+      where+        getVertex = \case+          AcyclicSCC v -> Seq.singleton v+          CyclicSCC vs -> Seq.fromList vs+++ 

@@ -3,6 +3,7 @@     Ann(..)   , TyTerm(..)   , termType+  , termSignature   , tyVarE   , tyPrimE   , tyAppE@@ -50,6 +51,9 @@ termType :: TyTerm prim loc v -> Type loc v termType (TyTerm (Fix (Ann ty _))) = ty +termSignature :: (Ord v, Eq loc) => TyTerm prim loc v -> Signature loc v+termSignature = typeToSignature . termType+ -- tyTerm :: Type loc v -> TermF loc var (Ann () ) -> TyTerm loc var tyTerm :: Type loc v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))) -> TyTerm prim loc v tyTerm ty x = TyTerm $ Fix $ Ann ty x@@ -89,7 +93,7 @@  -- | 'constrE' @loc ty tag arity@ constructs constructor tag expression. tyConstrE :: loc -> Type loc v -> v -> TyTerm prim loc v-tyConstrE loc ty tag = tyTerm ty $ Constr loc ty tag+tyConstrE loc ty tag = tyTerm ty $ Constr loc tag  -- | 'bottomE' @loc@ constructs bottom value. tyBottomE :: Type loc v -> loc -> TyTerm prim loc v@@ -106,33 +110,22 @@         Let loc v a  -> Let (f loc) (v { bind'loc = f $ bind'loc v }) a         LetRec loc vs a -> LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a         AssertType loc r sig -> AssertType (f loc) r (mapLoc f sig)-        Constr loc ty v -> Constr (f loc) (mapLoc f ty) v+        Constr loc v -> Constr (f loc) v         Case loc e alts -> Case (f loc) e (fmap (mapAlt f) alts)         Bottom loc -> Bottom (f loc)        mapAlt g alt@CaseAlt{..} = alt         { caseAlt'loc  = g caseAlt'loc-        , caseAlt'args = fmap (mapTyped g) caseAlt'args-        , caseAlt'constrType = mapLoc g caseAlt'constrType+        , caseAlt'args = fmap (first g) caseAlt'args         } -      mapTyped g (Typed ty val) = Typed (mapLoc g ty) (first g val)- instance TypeFunctor (TyTerm prim) where   mapType f (TyTerm x) = TyTerm $ foldFix go x     where       go (Ann ty term) = Fix $ Ann (f ty) $         case term of-          Constr loc cty cons -> Constr loc (f cty) cons-          Case loc e alts          -> Case loc e $ fmap applyAlt alts-          other                    -> other--      applyAlt alt@CaseAlt{..} = alt-        { caseAlt'args       = fmap applyTyped caseAlt'args-        , caseAlt'constrType = f caseAlt'constrType-        }--      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }+          AssertType loc r t -> AssertType loc r (f t)+          other              -> other  instance CanApply (TyTerm prim) where   apply subst term = mapType (apply subst) term

@@ -1,7 +1,7 @@ {-# LANGUAGE DeriveAnyClass     #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DerivingStrategies #-}--- | This module contains types for structured type errors.+-- | This module contains types for type errors. module Type.Check.HM.TypeError where  import Control.DeepSeq (NFData)@@ -19,8 +19,14 @@   | UnifyErr   loc (Type loc var) (Type loc var)  -- ^ Unification error   | SubtypeErr loc (Type loc var) (Type loc var)  -- ^ Subtype error (happens on explicit type assertions)   | NotInScopeErr loc var                         -- ^ Missing signature in context for free-variable.+  | ConsArityMismatch+      { consArityMismatch'loc :: loc+      , consArityMismatch'tag :: var+      , consArityMismatch'expected :: Int+      , consArityMismatch'actual   :: Int+      } -- ^ mismatch of arity in pattern-matching   | EmptyCaseExpr loc                             -- ^ no case alternatives in the case expression-  | FreshNameFound                                -- ^ internal error with fresh name substitution+  | FreshNameFound                                -- ^ internal error with fresh name substitution. Should not normally occur if algorithm is correct.   deriving stock    (Show, Eq, Functor, Generic, Data)   deriving anyclass (NFData) @@ -30,6 +36,7 @@     UnifyErr loc tA tB   -> UnifyErr (f loc) (mapLoc f tA) (mapLoc f tB)     SubtypeErr loc tA tB -> SubtypeErr (f loc) (mapLoc f tA) (mapLoc f tB)     NotInScopeErr loc v  -> NotInScopeErr (f loc) v+    ConsArityMismatch loc tag expect actual -> ConsArityMismatch (f loc)  tag expect actual     EmptyCaseExpr loc    -> EmptyCaseExpr (f loc)     FreshNameFound       -> FreshNameFound @@ -39,6 +46,7 @@     UnifyErr _ a b     -> tyVars a <> tyVars b     SubtypeErr _ a b   -> tyVars a <> tyVars b     NotInScopeErr _ _  -> mempty+    ConsArityMismatch _ _ _ _ -> mempty     EmptyCaseExpr _    -> mempty     FreshNameFound     -> mempty @@ -49,6 +57,7 @@     NotInScopeErr _ _  -> mempty     EmptyCaseExpr _    -> mempty     FreshNameFound     -> mempty+    ConsArityMismatch _ _ _ _ -> mempty  instance CanApply TypeError where   apply f = \case

@@ -1,5 +1,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeFamilies #-} -- | Tests for language with lambda calculus with numbers and booleans. module TM.NumLang where@@ -12,6 +13,8 @@ import qualified Type.Check.HM as T import qualified Data.Map.Strict as M +import Data.Text.Prettyprint.Doc+ infixr ~>  data CodeLoc = CodeLoc@@ -20,13 +23,21 @@   }   deriving (Show, Eq) +instance Pretty CodeLoc where+  pretty (CodeLoc row col) = hcat [pretty row, ":", pretty col]+ -- | Primitives of our language. -- We support integers and booleans data Prim-  = PInt CodeLoc Int     -- ^ integers-  | PBool CodeLoc Bool   -- ^ booleans+  = PInt Int     -- ^ integers+  | PBool Bool   -- ^ booleans   deriving (Show, Eq) +instance Pretty Prim where+  pretty = \case+    PInt  n -> pretty n+    PBool b -> pretty b+ -- | Type for variables type Var = String @@ -51,9 +62,9 @@   type Prim NumLang = Prim      -- ^ primitives    -- what type is assigned to primitive literals of the language-  getPrimType = \case-    PInt  loc _ -> T.conT loc "Int"  []-    PBool loc _ -> T.conT loc "Bool" []+  getPrimType loc = \case+    PInt  _ -> T.conT loc "Int"  []+    PBool _ -> T.conT loc "Bool" []  -- | Expressions for our language newtype Expr = Expr { unExpr :: T.Term Prim CodeLoc Var }@@ -67,11 +78,11 @@  -- | constructor for integer literals int :: Int -> Expr-int = Expr . T.primE defLoc . PInt defLoc+int = Expr . T.primE defLoc . PInt  -- | constructor for boolean literals bool :: Bool -> Expr-bool = Expr . T.primE defLoc . PBool defLoc+bool = Expr . T.primE defLoc . PBool  -- numeric expressions @@ -152,36 +163,75 @@ -- custom constructors  -- types for custom types-pointT, circleT, rectT :: Ty+pointT, circleT, rectT, colorT :: Ty pointT  = T.conT defLoc "Point" [] circleT = T.conT defLoc "Circle" [] rectT = T.conT defLoc "Rect" []+colorT = T.conT defLoc "Color" [] +maybeT :: Ty -> Ty+maybeT a = T.conT defLoc "Maybe" [a]+ -- | Point constructor point :: Expr -> Expr -> Expr-point = app2 (Expr $ T.constrE defLoc (intT ~> intT ~> pointT) "Point")+point = app2 (Expr $ T.constrE defLoc "Point")  circle :: Expr -> Expr -> Expr-circle = app2 (Expr $ T.constrE defLoc (pointT ~> intT ~> circleT) "Circle")+circle = app2 (Expr $ T.constrE defLoc "Circle")  rect :: Expr -> Expr -> Expr-rect = app2 (Expr $ T.constrE defLoc (pointT ~> pointT ~> rectT) "Rect")+rect = app2 (Expr $ T.constrE defLoc "Rect") +red, blue, green :: Expr+red   = Expr $ T.constrE defLoc "Red"+blue  = Expr $ T.constrE defLoc "Blue"+green = Expr $ T.constrE defLoc "Green"++just :: Expr -> Expr+just = app (Expr $ T.constrE defLoc "Just")++nothing :: Expr+nothing = Expr $ T.constrE defLoc "Nothing"+ casePoint :: Expr -> (Var, Var) -> Expr -> Expr casePoint (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e-  [T.CaseAlt defLoc "Point" [tyVar intT x, tyVar intT y] pointT body]+  [T.CaseAlt defLoc "Point" (caseArgs [x, y]) body]  caseCircle :: Expr -> (Var, Var) -> Expr -> Expr caseCircle (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e-  [T.CaseAlt defLoc "Circle" [tyVar pointT x, tyVar intT y] circleT body]+  [T.CaseAlt defLoc "Circle" (caseArgs [x, y]) body]  caseRect :: Expr -> (Var, Var) -> Expr -> Expr caseRect (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e-  [T.CaseAlt defLoc "Rect" [tyVar pointT x, tyVar pointT y] rectT body]+  [T.CaseAlt defLoc "Rect" (caseArgs [x, y]) body] -tyVar :: Ty -> Var -> T.Typed CodeLoc Var (CodeLoc, Var)-tyVar ty v = T.Typed ty (defLoc, v)+caseArgs :: [Var] -> [(CodeLoc, Var)]+caseArgs = fmap (\x -> (defLoc, x)) +data CaseColor = CaseColor+  { case'red   :: Expr+  , case'blue  :: Expr+  , case'green :: Expr+  }++caseColor :: Expr -> CaseColor -> Expr+caseColor (Expr e) CaseColor{..} = Expr $ T.caseE defLoc e+  [ T.CaseAlt defLoc "Red"   [] (unExpr $ case'red)+  , T.CaseAlt defLoc "Blue"  [] (unExpr $ case'blue)+  , T.CaseAlt defLoc "Green" [] (unExpr $ case'green)+  ]++data CaseMaybe = CaseMaybe+  { case'just    :: Expr -> Expr+  , case'nothing :: Expr+  }++caseMaybe :: Expr -> CaseMaybe -> Expr+caseMaybe (Expr e) CaseMaybe{..} = Expr $ T.caseE defLoc e+  [ T.CaseAlt defLoc "Just"    [(defLoc, "$justArg")] (unExpr $ case'just "$justArg")+  , T.CaseAlt defLoc "Nothing" []              (unExpr case'nothing)+  ]+ ---------------------------------------------------------- -- Type inference context --@@ -190,13 +240,29 @@  -- | Context contains types for all known definitions defContext :: T.Context CodeLoc Var-defContext = T.Context $ M.fromList $ mconcat-  [ booleans-  , nums-  , comparisons-  , [("if", forA $ T.monoT $ boolT ~> aT ~> aT ~> aT)]-  ]+defContext = T.Context+  { T.context'binds        = binds+  , T.context'constructors = cons+  }   where+    binds = M.fromList $ mconcat+      [ booleans+      , nums+      , comparisons+      , [("if", forA $ T.monoT $ boolT ~> aT ~> aT ~> aT)]+      ]++    cons = M.fromList+      [ "Point"  `is` (intT ~> intT ~> pointT)+      , "Circle" `is` (pointT ~> intT ~> circleT)+      , "Rect"   `is` (pointT ~> pointT ~> rectT)+      , "Red"    `is` colorT+      , "Blue"   `is` colorT+      , "Green"  `is` colorT+      , ("Just"    , forA $ T.monoT $ aT ~> maybeT aT)+      , ("Nothing" , forA $ T.monoT $ maybeT aT)+      ]+     booleans =       [ "&&"  `is` (boolT ~> boolT ~> boolT)       , "||"  `is` (boolT ~> boolT ~> boolT)@@ -230,6 +296,52 @@ boolExpr1 :: Expr boolExpr1 = andB (andB (notB ((intExpr1 `lte` 1000) `orB` (2 `gt` 0))) (bool True)) (5 `neq` (2 + 2)) +colorFun :: Expr+colorFun = lam "c" $ caseColor "c" CaseColor+  { case'red   = 1+  , case'blue  = 2+  , case'green = 3+  }++colorFun2 :: Expr+colorFun2 = lam "c" $ caseColor "c" CaseColor+  { case'red   = nothing+  , case'blue  = just $ bool True+  , case'green = just $ bool False+  }++colorFun3 :: Expr+colorFun3 = lam "c" $ caseColor "c" CaseColor+  { case'blue  = just $ bool True+  , case'green = just $ bool False+  , case'red   = nothing+  }++colorFun4 :: Expr+colorFun4 = lam "mc" $ caseMaybe "mc" CaseMaybe+  { case'just    = id+  , case'nothing = red+  }++colorFunFail :: Expr+colorFunFail = lam "c" $ caseColor "c" CaseColor+  { case'red   = 1+  , case'blue  = bool True+  , case'green = 3+  }++mapMaybe :: Expr+mapMaybe = lam "f" $ lam "ma" $ caseMaybe "ma" CaseMaybe+  { case'nothing = nothing+  , case'just    = \a -> just $ app "f" a+  }++bindMaybe :: Expr+bindMaybe = lam "ma" $ lam "mf" $ caseMaybe "ma" CaseMaybe+  { case'nothing = nothing+  , case'just    = \a -> app "mf" a+  }+ failExpr1 :: Expr failExpr1 = lam "x" $ 2 + "x" `eq` (bool True) @@ -319,9 +431,28 @@   , check "negate point"    (pointT ~> pointT)              negatePointLam   , check "rect square"     (rectT ~> intT)                 rectSquare   , check "inside circle 2" (circleT ~> pointT ~> boolT)    insideCircle2+  , check "color fun"       (colorT ~> intT)                colorFun+  , check "color fun 2"     (colorT ~> maybeT boolT)        colorFun2+  , check "color fun 3"     (colorT ~> maybeT boolT)        colorFun3+  , check "color fun 4"     (maybeT colorT ~> colorT)       colorFun4+  , check "map maybe"       ((aT ~> bT) ~> maybeT aT ~> maybeT bT) mapMaybe+  , check "bind maybe"      (maybeT aT ~> (aT ~> maybeT bT) ~> maybeT bT) bindMaybe+  , fails "color fun fail"  colorFunFail+  , checkList "list of expressions" [("a", intExpr1), ("b", boolExpr1), ("c", intFun1)]   ]   where+    aT = T.varT defLoc "a"+    bT = T.varT defLoc "b"+     infer = T.inferType defContext . unExpr     check msg ty expr = testCase msg $ Right ty @=? (infer expr)     fails msg expr = testCase msg $ assertBool "Detected wrong type" $ isLeft (infer expr)++    checkList msg exprs = testCase msg $ assertBool msg $ isRight (T.inferTermList defContext $ fmap (uncurry toBind) exprs)++----------------------------------------------------------++-- | Prints result of type-inference+printInfer :: Expr -> IO ()+printInfer (Expr e) = T.printInfer $ T.inferType defContext e 

@@ -35,7 +35,7 @@   type Src  TestLang = ()   type Var  TestLang = Text   type Prim TestLang = NoPrim-  getPrimType _ = error "No primops"+  getPrimType _ _ = error "No primops"  -- I combinator termI,termK :: Term NoPrim () Text