@@ -14,6 +14,7 @@ import Control.Applicative
1414import Control.Arrow (first, second)
1515import Control.Monad (unless)
1616import Control.Monad.Writer.Class
17+import Control.Monad.Supply.Class (MonadSupply, fresh, freshName)
1718
1819import Data.Function (on)
1920import Data.List (foldl', sortBy, nub)
@@ -45,7 +46,7 @@ data RedundancyError = Incomplete | Unknown
4546-- Qualifies a propername from a given qualified propername and a default module name
4647--
4748qualifyName
48− :: (ProperName a)
49+ :: ProperName a
4950 -> ModuleName
5051 -> Qualified (ProperName b)
5152 -> Qualified (ProperName a)
@@ -231,7 +232,7 @@ missingAlternative env mn ca uncovered
231232--
232233checkExhaustive
233234 :: forall m
234− . (MonadWriter MultipleErrors m)
235+ . (MonadWriter MultipleErrors m, MonadSupply m)
235236 => Environment
236237 -> ModuleName
237238 -> Int
@@ -262,7 +263,7 @@ checkExhaustive env mn numArgs cas expr = makeResult . first nub $ foldl' step (
262263 _ -> return ()
263264 if null bss
264265 then return expr
265− else return (addPartialConstraint (second null (splitAt 5 bss)) expr)
266+ else addPartialConstraint (second null (splitAt 5 bss)) expr
266267 where
267268 tellRedundant = tell . errorMessage . uncurry OverlappingPattern . second null . splitAt 5 $ bss'
268269 tellIncomplete = tell . errorMessage $ IncompleteExhaustivityCheck
@@ -273,34 +274,42 @@ checkExhaustive env mn numArgs cas expr = makeResult . first nub $ foldl' step (
273274 --
274275 -- The binder information is provided so that it can be embedded in the constraint,
275276 -- and then included in the error message.
276− addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
277− addPartialConstraint (bss, complete) e =
278− Let [ partial ] (App (Var (Qualified Nothing (Ident C.__unused))) e)
277+ addPartialConstraint :: MonadSupply m => ([[Binder]], Bool) -> Expr -> m Expr
278+ addPartialConstraint (bss, complete) e = do
279+ tyVar <- ("p" ++) . show <$> fresh
280+ var <- freshName
281+ return $
282+ Let
283+ [ partial var tyVar ]
284+ $ App (Var (Qualified Nothing (Ident C.__unused))) e
279285 where
280− partial :: Declaration
281− partial = ValueDeclaration (Ident C.__unused)
282− Private
283− []
284− (Right (TypedValue True (Abs (Left (Ident "x"))
285− (Var (Qualified Nothing (Ident "x"))))
286− ty))
287−
288− ty :: Type
289− ty = ForAll "a" (ConstrainedType [ Constraint (Qualified (Just (ModuleName [ProperName C.prim]))
290− (ProperName "Partial"))
291− []
292− (Just (PartialConstraintData (map (map prettyPrintBinderAtom) bss) complete))
293− ]
294− (TypeApp (TypeApp tyFunction (TypeVar "a"))
295− (TypeVar "a")))
296− Nothing
286+ partial :: String -> String -> Declaration
287+ partial var tyVar =
288+ ValueDeclaration (Ident C.__unused) Private [] $ Right $
289+ TypedValue
290+ True
291+ (Abs (Left (Ident var)) (Var (Qualified Nothing (Ident var))))
292+ (ty tyVar)
293+
294+ ty :: String -> Type
295+ ty tyVar =
296+ ForAll tyVar
297+ ( ConstrainedType
298+ [ Constraint C.Partial [] (Just constraintData) ]
299+ $ TypeApp (TypeApp tyFunction (TypeVar tyVar)) (TypeVar tyVar)
300+ )
301+ Nothing
302+
303+ constraintData :: ConstraintData
304+ constraintData =
305+ PartialConstraintData (map (map prettyPrintBinderAtom) bss) complete
297306
298307-- |
299308-- Exhaustivity checking
300309--
301310checkExhaustiveExpr
302311 :: forall m
303− . MonadWriter MultipleErrors m
312+ . (MonadWriter MultipleErrors m, MonadSupply m)
304313 => Environment
305314 -> ModuleName
306315 -> Expr