@@ -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
0 commit comments