haskell/src/SumTypes/ContinueAfterCheckFail.hs

-{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE RebindableSyntax #-}
-
 module SumTypes.ContinueAfterCheckFail where
 
-import Prelude hiding (Monad(..), (>=), (<=), lookup)
-import GHC.Exts (Constraint)
+import Prelude hiding ((>=), (<=), lookup, fail)
 import qualified Data.Map as Map
+import Control.Monad.Writer.Lazy (Writer)
+import qualified Control.Monad.Writer.Lazy as Writer
 
 import SumTypes.Language
 import Util.ErrorMessages
 import Util.PartialOrd
 
--- is needed because we use the RebindableSyntax extension
-ifThenElse :: Bool -> a -> a -> a
-ifThenElse True thn _ = thn
-ifThenElse False _ els = els
-
 type Error = [String]
-data Infer a = Inferred a | NotInferred Error
 
+type Infer a = Writer Error a
 type Check = Infer ()
 
-instance Functor Infer where
-  fmap _ (NotInferred err) = NotInferred err
-  fmap f (Inferred ty) = Inferred $ f ty
-
-instance Applicative Infer where
-  pure = Inferred
-  (NotInferred err) <*> _ = NotInferred err
-  (Inferred a) <*> something = fmap a something
-
 class WithTop a where
   top :: a
 
@@ -46,30 +30,10 @@ instance (WithTop a, WithTop b) => WithTop (a, b) where
 instance (WithTop v) => WithTop (Map.Map Name v) where
   top = Map.empty
 
--- Had to define an own monad type class.
--- It is not possible otherwise to get the type constraint WithTop a.
--- We use the extension ConstraintKinds to support this.
--- Could not find a simpler solution for this problem.
--- The restricted monad problem is common.
-class RMonad m where
-  type RMonadCtx m a :: Constraint
-  return :: RMonadCtx m a => a -> m a
-  (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
-  (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a ->  m b -> m b
-  m >> k = m >>= \_ -> k
-  fail :: [String] -> m a
-
-instance RMonad Infer where
-  type RMonadCtx Infer a = WithTop a
-  return = Inferred
-  (Inferred ty) >>= f = f ty
-  NotInferred err1 >>= f =
-    -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
-    case f top of
-      Inferred _ -> fail err1
-      NotInferred err2 -> fail $ err1 ++ err2
-  fail = NotInferred
-
+fail :: WithTop a => Error -> Infer a
+fail msg = do
+  Writer.tell msg
+  return top
 
 -- matching functions that extract the inner types if possible
 matchNat :: Type -> String -> Check

haskell/test/SumTypes/ContinueAfterFailSpec.hs

@@ -9,12 +9,13 @@ import SumTypes.Base as B
 import SumTypes.SharedSpecs
 import SumTypes.ContinueAfterCheckFail as C
 import SumTypes.Language
+import Control.Monad.Writer.Lazy (Writer, runWriter)
 
-
-instance ConvertToBInfer C.Infer where
-  convert (C.Inferred ty) = B.Inferred ty
-  convert (C.NotInferred err) = B.NotInferred $ head err
-
+instance ConvertToBInfer (Writer C.Error) where
+  convert m =
+    case runWriter m of
+      (t,[]) -> Inferred t
+      (t,err) -> NotInferred (head err)
 
 main :: IO ()
 main = hspec spec