checkGuardsForImpossibility :: (?globals :: Globals) => Span -> Id -> Checker ()
checkGuardsForImpossibility s name = do
  -- Get top of guard predicate stack
  st <- get
  let ps = head $ guardPredicates st

  -- Convert all universal variables to existential
  let tyVarContextExistential =
         mapMaybe (\(v, (k, q)) ->
                       case q of
                         BoundQ -> Nothing
                         _      -> Just (v, (k, InstanceQ))) (tyVarContext st)
  tyVars <- justCoeffectTypesConverted s tyVarContextExistential

  -- For each guard predicate
  forM_ ps $ \((ctxt, p), s) -> do

    -- Existentially quantify those variables occuring in the pattern in scope
    let thm = foldr (uncurry Exists) p ctxt

    debugM "impossibility" $ "about to try" <> pretty thm
    -- Try to prove the theorem
    result <- liftIO $ provePredicate thm tyVars

    p <- simplifyPred thm

    case result of
      QED -> return ()

      -- Various kinds of error
      -- TODO make errors better
      NotValid msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }
      NotValidTrivial unsats -> throw ImpossiblePatternMatchTrivial
        { errLoc = s
        , errId = name
        , errUnsats = unsats
        }
      Timeout -> throw SolverTimeout
        { errLoc = s
        , errDefId = name
        , errSolverTimeoutMillis = solverTimeoutMillis
        , errContext = "pattern match of an equation"
        , errPred = p
        }

      OtherSolverError msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }

      SolverProofError msg -> error msg
checkGuardsForImpossibility :: (?globals :: Globals) => Span -> Id -> Checker ()
checkGuardsForImpossibility s name = do
  -- Get top of guard predicate stack
  st <- get
  let ps = head $ guardPredicates st

  -- Convert all universal variables to existential
  let tyVarContextExistential =
         mapMaybe (\(v, (k, q)) ->
                       case q of
                         BoundQ -> Nothing
                         _      -> Just (v, (k, InstanceQ))) (tyVarContext st)
  tyVars <- justCoeffectTypesConverted s tyVarContextExistential

  -- For each guard predicate
  forM_ ps $ \((ctxt, p), s) -> do

    -- Existentially quantify those variables occuring in the pattern in scope
    let thm = foldr (uncurry Exists) p ctxt

    debugM "impossibility" $ "about to try" <> pretty thm
    -- Try to prove the theorem
    result <- liftIO $ provePredicate thm tyVars

    p <- simplifyPred thm

    case result of
      QED -> return ()

      -- Various kinds of error
      -- TODO make errors better
      NotValid msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }
      NotValidTrivial unsats -> throw ImpossiblePatternMatchTrivial
        { errLoc = s
        , errId = name
        , errUnsats = unsats
        }
      Timeout -> throw SolverTimeout
        { errLoc = s
        , errDefId = name
        , errSolverTimeoutMillis = solverTimeoutMillis
        , errContext = "pattern match of an equation"
        , errPred = p
        }

      OtherSolverError msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }

      SolverProofError msg -> error msg
checkGuardsForImpossibility s name = do
  -- Get top of guard predicate stack
  st <- get
  let ps = head $ guardPredicates st

  -- Convert all universal variables to existential
  let tyVarContextExistential =
         mapMaybe (\(v, (k, q)) ->
                       case q of
                         BoundQ -> Nothing
                         _      -> Just (v, (k, InstanceQ))) (tyVarContext st)
  tyVars <- justCoeffectTypesConverted s tyVarContextExistential

  -- For each guard predicate
  forM_ ps $ \((ctxt, p), s) -> do

    -- Existentially quantify those variables occuring in the pattern in scope
    let thm = foldr (uncurry Exists) p ctxt

    debugM "impossibility" $ "about to try" <> pretty thm
    -- Try to prove the theorem
    result <- liftIO $ provePredicate thm tyVars

    p <- simplifyPred thm

    case result of
      QED -> return ()

      -- Various kinds of error
      -- TODO make errors better
      NotValid msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }
      NotValidTrivial unsats -> throw ImpossiblePatternMatchTrivial
        { errLoc = s
        , errId = name
        , errUnsats = unsats
        }
      Timeout -> throw SolverTimeout
        { errLoc = s
        , errDefId = name
        , errSolverTimeoutMillis = solverTimeoutMillis
        , errContext = "pattern match of an equation"
        , errPred = p
        }

      OtherSolverError msg -> throw ImpossiblePatternMatch
        { errLoc = s
        , errId = name
        , errPred = p
        }

      SolverProofError msg -> error msg