@@ -14,6 +14,7 @@ import Control.Applicative
14import Control.Arrow (first, second)
14import Control.Arrow (first, second)
15import Control.Monad (unless)
15import Control.Monad (unless)
16import Control.Monad.Writer.Class
16import Control.Monad.Writer.Class
17+import Control.Monad.Supply.Class (MonadSupply, fresh, freshName)
18import Data.Function (on)
19import Data.Function (on)
19import Data.List (foldl', sortBy, nub)
20import Data.List (foldl', sortBy, nub)
@@ -45,7 +46,7 @@ data RedundancyError = Incomplete | Unknown
45-- Qualifies a propername from a given qualified propername and a default module name
46-- Qualifies a propername from a given qualified propername and a default module name
47qualifyName
48qualifyName
48− :: (ProperName a)
49+ :: ProperName a
49 -> ModuleName
50 -> ModuleName
50 -> Qualified (ProperName b)
51 -> Qualified (ProperName b)
51 -> Qualified (ProperName a)
52 -> Qualified (ProperName a)
@@ -231,7 +232,7 @@ missingAlternative env mn ca uncovered
232checkExhaustive
233checkExhaustive
233 :: forall m
234 :: forall m
234− . (MonadWriter MultipleErrors m)
235+ . (MonadWriter MultipleErrors m, MonadSupply m)
235 => Environment
236 => Environment
236 -> ModuleName
237 -> ModuleName
@@ -262,7 +263,7 @@ checkExhaustive env mn numArgs cas expr = makeResult . first nub $ foldl' step (
262 _ -> return ()
263 _ -> return ()
263 if null bss
264 if null bss
264 then return expr
265 then return expr
265− else return (addPartialConstraint (second null (splitAt 5 bss)) expr)
266+ else addPartialConstraint (second null (splitAt 5 bss)) expr
267 tellRedundant = tell . errorMessage . uncurry OverlappingPattern . second null . splitAt 5 $ bss'
268 tellRedundant = tell . errorMessage . uncurry OverlappingPattern . second null . splitAt 5 $ bss'
268 tellIncomplete = tell . errorMessage $ IncompleteExhaustivityCheck
269 tellIncomplete = tell . errorMessage $ IncompleteExhaustivityCheck
@@ -273,34 +274,42 @@ checkExhaustive env mn numArgs cas expr = makeResult . first nub $ foldl' step (
274 -- The binder information is provided so that it can be embedded in the constraint,
275 -- The binder information is provided so that it can be embedded in the constraint,
275 -- and then included in the error message.
276 -- and then included in the error message.
276− addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
277+ addPartialConstraint :: MonadSupply m => ([[Binder]], Bool) -> Expr -> m Expr
277− addPartialConstraint (bss, complete) e =
278+ addPartialConstraint (bss, complete) e = do
279+ tyVar <- ("p" ++) . show <$> fresh
283+ [ partial var tyVar ]
278− Let [ partial ] (App (Var (Qualified Nothing (Ident C.__unused))) e)
284+ $ App (Var (Qualified Nothing (Ident C.__unused))) e
280− partial :: Declaration
286+ partial :: String -> String -> Declaration
281− partial = ValueDeclaration (Ident C.__unused)
288+ ValueDeclaration (Ident C.__unused) Private [] $ Right $
284− (Right (TypedValue True (Abs (Left (Ident "x"))
289+ TypedValue
285− (Var (Qualified Nothing (Ident "x"))))
291+ (Abs (Left (Ident var)) (Var (Qualified Nothing (Ident var))))
288− ty :: Type
294+ ty :: String -> Type
289− ty = ForAll "a" (ConstrainedType [ Constraint (Qualified (Just (ModuleName [ProperName C.prim]))
295+ ty tyVar =
290− (ProperName "Partial"))
296+ ForAll tyVar
291− []
297+ ( ConstrainedType
298+ [ Constraint C.Partial [] (Just constraintData) ]
299+ $ TypeApp (TypeApp tyFunction (TypeVar tyVar)) (TypeVar tyVar)
303+ constraintData :: ConstraintData
292− (Just (PartialConstraintData (map (map prettyPrintBinderAtom) bss) complete))
305+ PartialConstraintData (map (map prettyPrintBinderAtom) bss) complete
294− (TypeApp (TypeApp tyFunction (TypeVar "a"))
299-- Exhaustivity checking
308-- Exhaustivity checking
301checkExhaustiveExpr
310checkExhaustiveExpr
302 :: forall m
311 :: forall m
303− . MonadWriter MultipleErrors m
312+ . (MonadWriter MultipleErrors m, MonadSupply m)
304 => Environment
313 => Environment
305 -> ModuleName
314 -> ModuleName