From 10f21fbabe41e712319a2a41200f983071d25ef2 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Wed, 5 Jun 2024 16:56:20 -0500
Subject: [PATCH] Display multiple example types for things with nontrivial
 (non-parametric) polymorphism (#388)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Closes #169.  Previously, we did this:
```
Disco> :type \x. x - 2
λx. x - 2 : ℤ → ℤ
```
However, this was a lie since in fact `\x. x - 2` is more general than that; but showing only one possible monomorphic type was still better than showing some generic monstrosity like `forall a. (N <: a, subtractive a) => a -> a`.

Now, with this PR, we do this:
```
Disco> :type \x. x - 2
This expression has multiple possible types.  Some examples:
λx. x - 2 : ℤ → ℤ
λx. x - 2 : ℚ → ℚ
```
See #169 for more context and examples.

Briefly, in this PR, we:
- Change the solver to return a *list* of solution substitutions instead of just a single one
- Add a "solution limit" counter to the solver so it can stop early once it has hit the limit for the number of solutions we want.
    - In some cases (e.g. when checking a provided type) we just want one.
    - In other cases (when inferring a type) we set an arbitrary bound of 16.
    - This is not really ideal --- in theory we would want to use some kind of proper backtracking logic monad like `LogicT` but that seems difficult/impossible to incorporate into `polysemy` (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy; https://github.com/polysemy-research/polysemy/issues/246).
- "Thin" the resulting list of solutions by throwing away any solutions which are supertypes of another solution in the list.
- Add pretty-printing that distinguishes between a single solution and multiple solutions

It is still possible to make the solver blow up in case there are many possible container variables to instantiate.  *e.g.* expressions like `\x. \y. \z. \w. (set(x), set(y), set(z), set(w))` take a very long time to typecheck.  I have some ideas for how to improve this situation, but for now it's an uncommon corner case.
---
 build                              |   2 +-
 feedback.yaml                      |   4 +-
 hie.yaml                           |  27 +--
 src/Disco/AST/Surface.hs           |   3 +-
 src/Disco/Effects/Input.hs         |  10 +-
 src/Disco/Interactive/Commands.hs  |  32 ++--
 src/Disco/Pretty.hs                |   5 +
 src/Disco/Typecheck.hs             | 165 ++++++++++++++----
 src/Disco/Typecheck/Constraints.hs |  33 ++--
 src/Disco/Typecheck/Solve.hs       | 270 ++++++++++++++++-------------
 src/Disco/Typecheck/Util.hs        |  39 +++--
 src/Disco/Util.hs                  |  38 +++-
 test/arith-basic-un/expected       |   2 +
 test/containers-each/expected      |  18 ++
 test/containers-reduce/expected    |   3 +
 test/graphs-basic/expected         |   3 +
 test/map-basic/expected            |  24 ++-
 test/poly-infer-sort/expected      |  18 +-
 test/poly-instantiate/expected     |  16 +-
 test/repl-ann/expected             |   2 +-
 test/repl-doc/expected             |   8 +
 test/table-function/expected       |  27 +++
 test/table-function/input          |   3 +-
 test/types-192/expected            |   3 +
 test/types-container/expected      |  21 +++
 test/types-naked-ops/expected      |  12 ++
 test/types-standalone-ops/expected |   2 +
 27 files changed, 545 insertions(+), 245 deletions(-)

diff --git a/build b/build
index 67938b0f..7044c32f 100755
--- a/build
+++ b/build
@@ -1,2 +1,2 @@
 #!/bin/sh
-stack test --fast --file-watch --test-arguments '--hide-successes +RTS -N8 -RTS'
+cabal test -j -O0
diff --git a/feedback.yaml b/feedback.yaml
index 10a06f60..fbd3cddd 100644
--- a/feedback.yaml
+++ b/feedback.yaml
@@ -1,3 +1,3 @@
 loops:
-  test8: stack test --fast --test-arguments '--hide-successes +RTS -N8 -RTS'
-  test30: stack test --fast --test-arguments '--hide-successes +RTS -N30 -RTS'
+  build: cabal -j build -O0
+  test: cabal -j test -O0 --test-show-details=direct
diff --git a/hie.yaml b/hie.yaml
index 5d3c001d..04cd2439 100644
--- a/hie.yaml
+++ b/hie.yaml
@@ -1,27 +1,2 @@
 cradle:
-  multi:
-    - path: "./explore"
-      config:
-        cradle:
-          none:
-    - path: "./nsf"
-      config:
-        cradle:
-          none:
-    - path: "./pubs"
-      config:
-        cradle:
-          none:
-    - path: "./notes"
-      config:
-        cradle:
-          none:
-    - path: "./example"
-      config:
-        cradle:
-          none:
-    - path: "./"
-      config:
-        cradle:
-          stack:
-            component: "disco:lib"
+  cabal:
diff --git a/src/Disco/AST/Surface.hs b/src/Disco/AST/Surface.hs
index bcb2e43e..3ea57456 100644
--- a/src/Disco/AST/Surface.hs
+++ b/src/Disco/AST/Surface.hs
@@ -632,7 +632,7 @@ containerDelims SetContainer = braces
 
 prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann)
 prettyBranches = \case
-  [] -> error "Empty branches are disallowed."
+  [] -> text ""
   b : bs ->
     pretty b
       $+$ foldr (($+$) . (text "," <+>) . pretty) empty bs
@@ -729,3 +729,4 @@ instance Pretty Pattern where
     PFrac p1 p2 ->
       withPA (getPA Div) $
         lt (pretty p1) <+> text "/" <+> rt (pretty p2)
+    PNonlinear p _ -> pretty p
diff --git a/src/Disco/Effects/Input.hs b/src/Disco/Effects/Input.hs
index 8af5b417..70468067 100644
--- a/src/Disco/Effects/Input.hs
+++ b/src/Disco/Effects/Input.hs
@@ -1,7 +1,3 @@
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Effects.Input
 -- Copyright   :  disco team and contributors
@@ -13,6 +9,7 @@
 module Disco.Effects.Input (
   module Polysemy.Input,
   inputToState,
+  mapInput,
 )
 where
 
@@ -23,3 +20,8 @@ import Polysemy.State
 -- | Run an input effect in terms of an ambient state effect.
 inputToState :: forall s r a. Member (State s) r => Sem (Input s ': r) a -> Sem r a
 inputToState = interpret (\case Input -> get @s)
+
+-- | Use a function to (contravariantly) transform the input value in
+--   an input effect.
+mapInput :: forall s t r a. Member (Input s) r => (s -> t) -> Sem (Input t ': r) a -> Sem r a
+mapInput f = interpret (\case Input -> inputs @s f)
diff --git a/src/Disco/Interactive/Commands.hs b/src/Disco/Interactive/Commands.hs
index 0543be1d..191b6f1d 100644
--- a/src/Disco/Interactive/Commands.hs
+++ b/src/Disco/Interactive/Commands.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
@@ -33,8 +34,9 @@ import Data.Bifunctor (second)
 import Data.Char (isSpace)
 import Data.Coerce
 import Data.List (find, isPrefixOf, sortBy, transpose)
+import Data.List.NonEmpty qualified as NE
 import Data.Map ((!))
-import qualified Data.Map as M
+import Data.Map qualified as M
 import Data.Maybe (mapMaybe, maybeToList)
 import Data.Typeable
 import Disco.AST.Surface
@@ -43,6 +45,7 @@ import Disco.Compile
 import Disco.Context as Ctx
 import Disco.Desugar
 import Disco.Doc
+import Disco.Effects.Fresh (runFresh)
 import Disco.Effects.Input
 import Disco.Effects.LFresh
 import Disco.Effects.State
@@ -66,7 +69,7 @@ import Disco.Parser (
   withExts,
  )
 import Disco.Pretty hiding (empty, (<>))
-import qualified Disco.Pretty as PP
+import Disco.Pretty qualified as PP
 import Disco.Property (prettyTestResult)
 import Disco.Syntax.Operators
 import Disco.Syntax.Prims (
@@ -84,8 +87,8 @@ import Polysemy.Output
 import Polysemy.Reader
 import System.FilePath (splitFileName)
 import Text.Megaparsec hiding (State, runParser)
-import qualified Text.Megaparsec.Char as C
-import qualified Text.PrettyPrint.Boxes as B
+import Text.Megaparsec.Char qualified as C
+import Text.PrettyPrint.Boxes qualified as B
 import Unbound.Generics.LocallyNameless (
   Name,
   name2String,
@@ -307,7 +310,7 @@ handleAnn ::
   REPLExpr 'CAnn ->
   Sem r ()
 handleAnn (Ann t) = do
-  (at, _) <- typecheckTop $ inferTop t
+  (at, _) <- typecheckTop $ inferTop1 t
   infoPretty at
 
 ------------------------------------------------------------
@@ -330,7 +333,7 @@ handleCompile ::
   REPLExpr 'CCompile ->
   Sem r ()
 handleCompile (Compile t) = do
-  (at, _) <- typecheckTop $ inferTop t
+  (at, _) <- typecheckTop $ inferTop1 t
   infoPretty . compileTerm $ at
 
 ------------------------------------------------------------
@@ -353,7 +356,7 @@ handleDesugar ::
   REPLExpr 'CDesugar ->
   Sem r ()
 handleDesugar (Desugar t) = do
-  (at, _) <- typecheckTop $ inferTop t
+  (at, _) <- typecheckTop $ inferTop1 t
   info $ pretty' . eraseDTerm . runDesugar . desugarTerm $ at
 
 ------------------------------------------------------------
@@ -802,7 +805,7 @@ tableCmd =
 
 handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r ()
 handleTable (Table t) = do
-  (at, ty) <- inputToState . typecheckTop $ inferTop t
+  (at, ty) <- inputToState . typecheckTop $ inferTop1 t
   v <- mapError EvalErr . evalTerm False $ at
 
   tydefs <- use @TopInfo (replModInfo . to allTydefs)
@@ -1026,13 +1029,22 @@ typeCheckCmd =
     , parser = TypeCheck <$> parseTermOrOp
     }
 
+maxInferredTypes :: Int
+maxInferredTypes = 16
+
 handleTypeCheck ::
   Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
   REPLExpr 'CTypeCheck ->
   Sem r ()
 handleTypeCheck (TypeCheck t) = do
-  (_, sig) <- typecheckTop $ inferTop t
-  info $ pretty' t <+> text ":" <+> pretty' sig
+  asigs <- typecheckTop $ inferTop maxInferredTypes t
+  sigs <- runFresh . mapInput (view (replModInfo . miTydefs)) $ thin $ NE.map snd asigs
+  let (toShow, extra) = NE.splitAt 8 sigs
+  when (length sigs > 1) $ info "This expression has multiple possible types.  Some examples:"
+  info $
+    vcat $
+      map (\sig -> pretty' t <+> text ":" <+> pretty' sig) toShow
+        ++ ["..." | not (P.null extra)]
 
 ------------------------------------------------------------
 
diff --git a/src/Disco/Pretty.hs b/src/Disco/Pretty.hs
index 51366ab3..22735bcb 100644
--- a/src/Disco/Pretty.hs
+++ b/src/Disco/Pretty.hs
@@ -24,6 +24,8 @@ import Prelude hiding ((<>))
 
 import Data.Bifunctor
 import Data.Char (isAlpha)
+import Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as NE
 import Data.Map (Map)
 import qualified Data.Map as M
 import Data.Ratio
@@ -93,6 +95,9 @@ pretty' = runReader initPA . runLFresh . pretty
 instance Pretty a => Pretty [a] where
   pretty = brackets . intercalate "," . map pretty
 
+instance Pretty a => Pretty (NonEmpty a) where
+  pretty = pretty . NE.toList
+
 instance (Pretty k, Pretty v) => Pretty (Map k v) where
   pretty m = do
     let es = map (\(k, v) -> pretty k <+> "->" <+> pretty v) (M.assocs m)
diff --git a/src/Disco/Typecheck.hs b/src/Disco/Typecheck.hs
index 7c90bcc1..f105d5ae 100644
--- a/src/Disco/Typecheck.hs
+++ b/src/Disco/Typecheck.hs
@@ -15,7 +15,7 @@ module Disco.Typecheck where
 
 import Control.Arrow ((&&&))
 import Control.Lens ((^..))
-import Control.Monad (forM_, unless, when, zipWithM)
+import Control.Monad (filterM, forM_, replicateM, unless, when, zipWithM)
 import Control.Monad.Trans.Maybe
 import Data.Bifunctor (first)
 import Data.Coerce
@@ -41,13 +41,16 @@ import qualified Disco.Subst as Subst
 import Disco.Syntax.Operators
 import Disco.Syntax.Prims
 import Disco.Typecheck.Constraints
+import Disco.Typecheck.Solve (SolutionLimit (..), solveConstraint)
 import Disco.Typecheck.Util
 import Disco.Types
 import Disco.Types.Rules
 import Polysemy hiding (embed)
 import Polysemy.Error
+import Polysemy.Input
 import Polysemy.Output
 import Polysemy.Reader
+import Polysemy.State (evalState)
 import Polysemy.Writer
 import Text.EditDistance (defaultEditCosts, restrictedDamerauLevenshteinDistance)
 import Unbound.Generics.LocallyNameless (
@@ -141,7 +144,7 @@ checkModule name imports (Module es _ m docs terms) = do
         (x : _) -> throw $ noLoc $ DuplicateDefns (coerce x)
         [] -> do
           aprops <- mapError noLoc $ checkProperties docCtx -- XXX location?
-          aterms <- mapError noLoc $ mapM inferTop terms -- XXX location?
+          aterms <- mapError noLoc $ mapM inferTop1 terms -- XXX location?
           return $ ModuleInfo name imports (map ((name .-) . getDeclName) typeDecls) docCtx aprops tyCtx tyDefnCtx defnCtx aterms es
  where
   getDefnName :: Defn -> Name ATerm
@@ -279,6 +282,8 @@ checkDefn ::
   TermDefn ->
   Sem r Defn
 checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $ do
+  debug "======================================================================"
+  debug "Checking definition:"
   -- Check that all clauses have the same number of patterns
   checkNumPats clauses
 
@@ -293,11 +298,11 @@ checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $
   -- patterns, and lazily unrolling type definitions along the way.
   (patTys, bodyTy) <- decomposeDefnTy (numPats (NE.head clauses)) ty
 
-  ((acs, _), theta) <- solve $ do
+  ((acs, _), thetas) <- solve 1 $ do
     aclauses <- forAll nms $ mapM (checkClause patTys bodyTy) clauses
     return (aclauses, ty)
 
-  return $ applySubst theta (Defn (coerce x) patTys bodyTy acs)
+  return $ applySubst (NE.head thetas) (Defn (coerce x) patTys bodyTy acs)
  where
   numPats = length . fst . unsafeUnbind
 
@@ -309,7 +314,7 @@ checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $
     -- patterns don't match across different clauses
     | otherwise = return ()
 
-  -- \| Check a clause of a definition against a list of pattern types and a body type.
+  -- Check a clause of a definition against a list of pattern types and a body type.
   checkClause ::
     Members '[Reader TyCtx, Reader TyDefCtx, Writer Constraint, Error TCError, Fresh] r =>
     [Type] ->
@@ -357,9 +362,12 @@ checkProperty ::
   Property ->
   Sem r AProperty
 checkProperty prop = do
-  (at, theta) <- solve $ check prop TyProp
+  debug "======================================================================"
+  debug "Checking property:"
+  debugPretty prop
+  (at, thetas) <- solve 1 $ check prop TyProp
   -- XXX do we need to default container variables here?
-  return $ applySubst theta at
+  return $ applySubst (NE.head thetas) at
 
 ------------------------------------------------------------
 -- Type checking/inference
@@ -446,33 +454,86 @@ infer ::
   Sem r ATerm
 infer = typecheck Infer
 
--- | Top-level type inference algorithm: infer a (polymorphic) type
---   for a term by running type inference, solving the resulting
---   constraints, and quantifying over any remaining type variables.
-inferTop ::
+-- | Top-level type inference algorithm, returning only the first
+--   possible result.
+inferTop1 ::
   Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
   Term ->
   Sem r (ATerm, PolyType)
-inferTop t = do
+inferTop1 t = NE.head <$> inferTop 1 t
+
+-- | Top-level type inference algorithm: infer up to the requested max
+--   number of possible (polymorphic) types for a term by running type
+--   inference, solving the resulting constraints, and quantifying
+--   over any remaining type variables.
+inferTop ::
+  Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r =>
+  Int ->
+  Term ->
+  Sem r (NonEmpty (ATerm, PolyType))
+inferTop lim t = do
   -- Run inference on the term and try to solve the resulting
   -- constraints.
-  (at, theta) <- solve $ infer t
+  debug "======================================================================"
+  debug "Inferring the type of:"
+  debugPretty t
+  (at, thetas) <- solve lim $ infer t
 
   debug "Final annotated term (before substitution and container monomorphizing):"
   debugPretty at
 
-  -- Apply the resulting substitution.
-  let at' = applySubst theta at
+  -- Currently the following code generates *every possible*
+  -- combination of substitutions for container variables, which can
+  -- lead to exponential blowup in some cases.  For example, inferring
+  -- the type of
+  --
+  --   \x. \y. \z. (set(x), set(y), set(z))
+  --
+  -- takes a Very Long Time.  Potential solutions include:
+  --
+  --   1. Do something similar as in the 'solve' function, using a State SolutionLimit
+  --      effect to stop early once we've generated enough variety.
+  --
+  --   2. Use a proper backtracking search monad like LogicT to scope
+  --      over both the generation of solution substitutions *and*
+  --      choosing container variable monomorphizations, then just
+  --      take a limited number of solutions.  Unfortunately,
+  --      polysemy's NonDet effect seems to be somewhat broken
+  --      (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy
+  --      ; https://github.com/polysemy-research/polysemy/issues/246 )
+  --      and using LogicT on top of Sem is going to be tedious since
+  --      it would require calling 'lift' on almost everything.
+  --
+  --   3. Also, it is probably (?) the case that no matter which of
+  --      the generated substitutions is used, the exact same
+  --      container variables are still unconstrained in all of them.
+  --      So we should be able to pick container variable
+  --      monomorphizations independently of the substitutions from
+  --      the solver.  Doing this would help though it would not
+  --      address the fundamental issue.
+
+  -- Quantify over any remaining type variables and return
+  -- the term along with the resulting polymorphic type.
+  return $ do
+    -- Monad NonEmpty
 
-      -- Find any remaining container variables.
-      cvs = containerVars (getType at')
+    -- Iterate over all possible solutions...
+    theta <- thetas
 
-      -- Replace them all with List.
-      at'' = applySubst (Subst.fromList $ map (,TyAtom (ABase CtrList)) (S.toList cvs)) at'
+    let -- Apply each one...
+        at' = applySubst theta at
 
-  -- Finally, quantify over any remaining type variables and return
-  -- the term along with the resulting polymorphic type.
-  return (at'', closeType (getType at''))
+        -- Find any remaining container variables...
+        cvs = containerVars (getType at')
+
+    -- Build all possible substitutions for those container variables...
+    ctrs <- replicateM (S.size cvs) (NE.map (TyAtom . ABase) (CtrList :| [CtrBag, CtrSet]))
+
+    -- Substitute for the container variables...
+    let at'' = applySubst (Subst.fromList $ zip (S.toList cvs) ctrs) at'
+
+    -- Return the term along with its type, with all substitutions applied.
+    return (at'', closeType (getType at''))
 
 -- | Top-level type checking algorithm: check that a term has a given
 --   polymorphic type by running type checking and solving the
@@ -483,8 +544,12 @@ checkTop ::
   PolyType ->
   Sem r ATerm
 checkTop t ty = do
-  (at, theta) <- solve $ checkPolyTy t ty
-  return $ applySubst theta at
+  debug "======================================================================"
+  debug "Checking the type of:"
+  debugPretty t
+  debugPretty ty
+  (at, theta) <- solve 1 $ checkPolyTy t ty
+  return $ applySubst (NE.head theta) at
 
 --------------------------------------------------
 -- The typecheck function
@@ -730,7 +795,7 @@ typecheck Infer (TPrim prim) = do
     c <- freshAtom
     a <- freshTy
     constraint $
-      COr
+      cOr
         [ CEq (TyAtom (ABase CtrBag)) (TyAtom c)
         , CEq (TyAtom (ABase CtrSet)) (TyAtom c)
         ]
@@ -745,7 +810,7 @@ typecheck Infer (TPrim prim) = do
     a <- freshTy
     c <- freshAtom
     constraint $
-      COr
+      cOr
         [ CEq (TyAtom (ABase CtrBag)) (TyAtom c)
         , CEq (TyAtom (ABase CtrSet)) (TyAtom c)
         ]
@@ -829,7 +894,7 @@ typecheck Infer (TPrim prim) = do
 
     -- b can be either Nat (a binomial coefficient)
     -- or a list of Nat (a multinomial coefficient).
-    constraint $ COr [CEq b TyN, CEq b (TyList TyN)]
+    constraint $ cOr [CEq b TyN, CEq b (TyList TyN)]
     return $ TyN :*: b :->: TyN
 
   ----------------------------------------
@@ -908,7 +973,7 @@ typecheck Infer (TPrim prim) = do
   inferPrim PrimAbs = do
     argTy <- freshTy
     resTy <- freshTy
-    cAbs argTy resTy `cOr` cSize argTy resTy
+    cAbs argTy resTy `orElse` cSize argTy resTy
     return $ argTy :->: resTy
 
   ----------------------------------------
@@ -932,7 +997,7 @@ typecheck Infer (TPrim prim) = do
 
     constraint $ CQual QCmp a
     constraint $
-      COr
+      cOr
         [ CEq (TyAtom (ABase CtrSet)) (TyAtom c)
         , CEq (TyAtom (ABase CtrBag)) (TyAtom c)
         ]
@@ -1483,7 +1548,7 @@ cPos ty = do
       -- Valid types for absolute value are Z -> N, Q -> F, or T -> T
       -- (e.g. Z5 -> Z5).
       constraint $
-        COr
+        cOr
           [ cAnd [CSub ty TyZ, CSub TyN res]
           , cAnd [CSub ty TyQ, CSub TyF res]
           , CEq ty res
@@ -1512,7 +1577,7 @@ cInt ty = do
       -- Valid types for absolute value are F -> N, Q -> Z, or T -> T
       -- (e.g. Z5 -> Z5).
       constraint $
-        COr
+        cOr
           [ cAnd [CSub ty TyF, CSub TyN res]
           , cAnd [CSub ty TyQ, CSub TyZ res]
           , CEq ty res
@@ -1544,7 +1609,7 @@ cExp ty1 ty2 = do
   -- to support multiplication, or else the exponent is Z, in which
   -- case the result type also has to support division.
   constraint $
-    COr
+    cOr
       [ cAnd [CQual QNum resTy, CEq ty2 TyN]
       , cAnd [CQual QDiv resTy, CEq ty2 TyZ]
       ]
@@ -1716,3 +1781,39 @@ ensureEq :: Member (Writer Constraint) r => Type -> Type -> Sem r ()
 ensureEq ty1 ty2
   | ty1 == ty2 = return ()
   | otherwise = constraint $ CEq ty1 ty2
+
+------------------------------------------------------------
+-- Subtyping
+------------------------------------------------------------
+
+isSubPolyType ::
+  Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
+  PolyType ->
+  PolyType ->
+  Sem r Bool
+isSubPolyType (Forall b1) (Forall b2) = do
+  (as1, ty1) <- unbind b1
+  (as2, ty2) <- unbind b2
+  let c = CAll (bind as1 (CSub ty1 (substs (zip as2 (map TyVar as1)) ty2)))
+  debug "======================================================================"
+  debug "Checking subtyping..."
+  debugPretty (Forall b1)
+  debugPretty (Forall b2)
+  ss <- runError (evalState (SolutionLimit 1) (solveConstraint c))
+  return (either (const False) (not . P.null) ss)
+
+thin :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType)
+thin = fmap NE.fromList . thin' . NE.toList
+
+-- Intuitively, this will always return a nonempty list given a nonempty list as input;
+-- we could probably rewrite it in terms of NonEmpty combinators but it's more effort than
+-- I cared to spend at the moment.
+thin' :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => [PolyType] -> Sem r [PolyType]
+thin' [] = return []
+thin' (ty : tys) = do
+  ss <- or <$> mapM (`isSubPolyType` ty) tys
+  if ss
+    then thin' tys
+    else do
+      tys' <- filterM (fmap not . (ty `isSubPolyType`)) tys
+      (ty :) <$> thin' tys'
diff --git a/src/Disco/Typecheck/Constraints.hs b/src/Disco/Typecheck/Constraints.hs
index ea669e98..0b7cc3da 100644
--- a/src/Disco/Typecheck/Constraints.hs
+++ b/src/Disco/Typecheck/Constraints.hs
@@ -1,10 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE OverloadedStrings #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Typecheck.Constraints
 -- Copyright   :  disco team and contributors
@@ -16,20 +12,20 @@
 module Disco.Typecheck.Constraints (
   Constraint (..),
   cAnd,
+  cOr,
 )
 where
 
+import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import Data.Semigroup
-import GHC.Generics (Generic)
-import Unbound.Generics.LocallyNameless hiding (lunbind)
-
 import Disco.Effects.LFresh
-
 import Disco.Pretty hiding ((<>))
 import Disco.Syntax.Operators (BFixity (In, InL, InR))
 import Disco.Types
 import Disco.Types.Rules
+import GHC.Generics (Generic)
+import Unbound.Generics.LocallyNameless hiding (lunbind)
 
 -- | Constraints are generated as a result of type inference and checking.
 --   These constraints are accumulated during the inference and checking phase
@@ -38,9 +34,9 @@ data Constraint where
   CSub :: Type -> Type -> Constraint
   CEq :: Type -> Type -> Constraint
   CQual :: Qualifier -> Type -> Constraint
-  CAnd :: [Constraint] -> Constraint
+  CAnd :: NonEmpty Constraint -> Constraint
   CTrue :: Constraint
-  COr :: [Constraint] -> Constraint
+  COr :: NonEmpty Constraint -> Constraint
   CAll :: Bind [Name Type] Constraint -> Constraint
   deriving (Show, Generic, Alpha, Subst Type)
 
@@ -49,14 +45,10 @@ instance Pretty Constraint where
     CSub ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "<:" <+> rt (pretty ty2)
     CEq ty1 ty2 -> withPA (PA 4 In) $ lt (pretty ty1) <+> "=" <+> rt (pretty ty2)
     CQual q ty -> withPA (PA 10 InL) $ lt (pretty q) <+> rt (pretty ty)
-    CAnd [c] -> pretty c
-    -- Use rt for both, since we don't need to print parens for /\ at all
-    CAnd (c : cs) -> withPA (PA 3 InR) $ rt (pretty c) <+> "/\\" <+> rt (pretty (CAnd cs))
-    CAnd [] -> "True"
+    -- Use rt for everything, since we don't need to print parens for /\ at all
+    CAnd cs -> withPA (PA 3 InR) $ foldr1 (\a b -> a <+> "/\\" <+> b) (NE.map (rt . pretty) cs)
     CTrue -> "True"
-    COr [c] -> pretty c
-    COr (c : cs) -> withPA (PA 2 InR) $ lt (pretty c) <+> "\\/" <+> rt (pretty (COr cs))
-    COr [] -> "False"
+    COr cs -> withPA (PA 2 InR) $ foldr1 (\a b -> lt a <+> "\\/" <+> rt b) (NE.map pretty cs)
     CAll b -> lunbind b $ \(xs, c) ->
       "∀" <+> intercalate "," (map pretty xs) <> "." <+> pretty c
 
@@ -65,11 +57,16 @@ cAnd :: [Constraint] -> Constraint
 cAnd cs = case filter nontrivial cs of
   [] -> CTrue
   [c] -> c
-  cs' -> CAnd cs'
+  (c : cs') -> CAnd (c :| cs')
  where
   nontrivial CTrue = False
   nontrivial _ = True
 
+cOr :: [Constraint] -> Constraint
+cOr [] = error "Empty list of constraints in cOr"
+cOr [c] = c
+cOr (c : cs) = COr (c :| cs)
+
 instance Semigroup Constraint where
   c1 <> c2 = cAnd [c1, c2]
   sconcat = cAnd . NE.toList
diff --git a/src/Disco/Typecheck/Solve.hs b/src/Disco/Typecheck/Solve.hs
index 5d00e431..43d19b36 100644
--- a/src/Disco/Typecheck/Solve.hs
+++ b/src/Disco/Typecheck/Solve.hs
@@ -1,11 +1,8 @@
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
-
 -- |
 -- Module      :  Disco.Typecheck.Solve
 -- Copyright   :  disco team and contributors
@@ -27,13 +24,11 @@ import Unbound.Generics.LocallyNameless (
   substs,
  )
 
-import Data.Coerce
-import GHC.Generics (Generic)
-
 import Control.Arrow ((&&&), (***))
 import Control.Lens hiding (use, (%=), (.=))
-import Control.Monad (unless, zipWithM)
+import Control.Monad (forM, join, unless, zipWithM)
 import Data.Bifunctor (first, second)
+import Data.Coerce
 import Data.Either (partitionEithers)
 import Data.List (
   find,
@@ -41,36 +36,39 @@ import Data.List (
   intersect,
   partition,
  )
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.List.NonEmpty qualified as NE
 import Data.Map (Map, (!))
-import qualified Data.Map as M
+import Data.Map qualified as M
 import Data.Maybe (
   fromJust,
   fromMaybe,
   mapMaybe,
  )
 import Data.Monoid (First (..))
+import Data.Semigroup (sconcat)
 import Data.Set (Set)
-import qualified Data.Set as S
+import Data.Set qualified as S
 import Data.Tuple
-
 import Disco.Effects.Fresh
 import Disco.Effects.State
-import Polysemy
-import Polysemy.Error
-import Polysemy.Input
-import Polysemy.Output
-
 import Disco.Messages
 import Disco.Pretty hiding ((<>))
 import Disco.Subst
-import qualified Disco.Subst as Subst
+import Disco.Subst qualified as Subst
 import Disco.Typecheck.Constraints
 import Disco.Typecheck.Graph (Graph)
-import qualified Disco.Typecheck.Graph as G
+import Disco.Typecheck.Graph qualified as G
 import Disco.Typecheck.Unify
 import Disco.Types
 import Disco.Types.Qualifiers
 import Disco.Types.Rules
+import Disco.Util (partitionEithersNE)
+import GHC.Generics (Generic)
+import Polysemy
+import Polysemy.Error
+import Polysemy.Input
+import Polysemy.Output
 
 --------------------------------------------------
 -- Solver errors
@@ -91,26 +89,44 @@ instance Semigroup SolveError where
 --------------------------------------------------
 -- Error utilities
 
-runSolve :: Sem (Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
-runSolve = runError . runFresh
+runSolve :: SolutionLimit -> Sem (State SolutionLimit ': Fresh ': Error SolveError ': r) a -> Sem r (Either SolveError a)
+runSolve lim = runError . runFresh . evalState lim
 
 -- | Run a list of actions, and return the results from those which do
 --   not throw an error.  If all of them throw an error, rethrow the
 --   first one.
-filterErrors :: Member (Error e) r => [Sem r a] -> Sem r [a]
+filterErrors :: Member (Error e) r => NonEmpty (Sem r a) -> Sem r (NonEmpty a)
 filterErrors ms = do
   es <- mapM try ms
-  case partitionEithers es of
-    (e : _, []) -> throw e
-    (_, as) -> return as
-
--- | A variant of 'asum' which picks the first action that succeeds,
---   or re-throws the error of the last one if none of them
---   do. Precondition: the list must not be empty.
-asum' :: Member (Error e) r => [Sem r a] -> Sem r a
-asum' [] = error "Impossible: asum' []"
-asum' [m] = m
-asum' (m : ms) = m `catch` (\_ -> asum' ms)
+  case partitionEithersNE es of
+    Left (e :| _) -> throw e
+    Right (_, as) -> return as
+
+--------------------------------------------------
+-- Solution limits
+
+-- | Max number of solutions to generate.
+newtype SolutionLimit = SolutionLimit {getSolutionLimit :: Int}
+
+-- | Register the fact that we found one solution, by decrementing the
+--   solution limit.
+countSolution :: Member (State SolutionLimit) r => Sem r ()
+countSolution = modify (SolutionLimit . subtract 1 . getSolutionLimit)
+
+-- | Run a subcomputation conditional on the solution limit still
+--   being positive.  If the solution limit has reached zero, stop
+--   early.
+withSolutionLimit ::
+  (Member (State SolutionLimit) r, Member (Output (Message ann)) r, Monoid a) =>
+  Sem r a ->
+  Sem r a
+withSolutionLimit m = do
+  SolutionLimit lim <- get
+  case lim of
+    0 -> do
+      debug "Reached solution limit, stopping early..."
+      return mempty
+    _ -> m
 
 --------------------------------------------------
 -- Simple constraints
@@ -249,15 +265,16 @@ lkup messg m k = fromMaybe (error errMsg) (M.lookup k m)
 -- Top-level solver algorithm
 
 solveConstraint ::
-  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r =>
   Constraint ->
-  Sem r S
+  Sem r (NonEmpty S)
 solveConstraint c = do
   -- Step 1. Open foralls (instantiating with skolem variables) and
   -- collect wanted qualifiers; also expand disjunctions.  Result in a
   -- list of possible constraint sets; each one consists of equational
   -- and subtyping constraints in addition to qualifiers.
 
+  debug "============================================================"
   debug "Solving:"
   debugPretty c
 
@@ -266,16 +283,17 @@ solveConstraint c = do
 
   qcList <- decomposeConstraint c
 
-  -- Now try continuing with each set and pick the first one that has
-  -- a solution.
-  asum' (map (uncurry solveConstraintChoice) qcList)
+  -- Now try continuing with each set.
+  sconcat <$> filterErrors (NE.map (uncurry solveConstraintChoice) qcList)
 
 solveConstraintChoice ::
-  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r =>
   TyVarInfoMap ->
   [SimpleConstraint] ->
-  Sem r S
+  Sem r (NonEmpty S)
 solveConstraintChoice quals cs = do
+  debug "solveConstraintChoice"
+
   debugPretty quals
   debug $ vcat (map pretty' cs)
 
@@ -387,16 +405,19 @@ solveConstraintChoice quals cs = do
   debug "------------------------------"
   debug "Solving for type variables..."
 
-  theta_sol <- solveGraph vm' g'''
-  debugPretty theta_sol
+  theta_sols <- solveGraph vm' g'''
+  case NE.nonEmpty theta_sols of
+    Nothing -> throw NoUnify
+    Just theta_sols_NE -> do
+      debugPretty theta_sols
 
-  debug "------------------------------"
-  debug "Composing final substitution..."
+      debug "------------------------------"
+      debug "Composing final substitution..."
 
-  let theta_final = theta_sol @@ theta_cyc @@ theta_skolem @@ theta_simp
-  debugPretty theta_final
+      let theta_finals = NE.map (@@ (theta_cyc @@ theta_skolem @@ theta_simp)) theta_sols_NE
+      debugPretty theta_finals
 
-  return theta_final
+      return theta_finals
 
 --------------------------------------------------
 -- Step 1. Constraint decomposition.
@@ -404,20 +425,20 @@ solveConstraintChoice quals cs = do
 decomposeConstraint ::
   Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
   Constraint ->
-  Sem r [(TyVarInfoMap, [SimpleConstraint])]
-decomposeConstraint (CSub t1 t2) = return [(mempty, [t1 :<: t2])]
-decomposeConstraint (CEq t1 t2) = return [(mempty, [t1 :=: t2])]
-decomposeConstraint (CQual q ty) = (: []) . (,[]) <$> decomposeQual ty q
-decomposeConstraint (CAnd cs) = map mconcat . sequence <$> mapM decomposeConstraint cs
-decomposeConstraint CTrue = return [mempty]
+  Sem r (NonEmpty (TyVarInfoMap, [SimpleConstraint]))
+decomposeConstraint (CSub t1 t2) = return $ NE.singleton (mempty, [t1 :<: t2])
+decomposeConstraint (CEq t1 t2) = return $ NE.singleton (mempty, [t1 :=: t2])
+decomposeConstraint (CQual q ty) = NE.singleton . (,[]) <$> decomposeQual ty q
+decomposeConstraint (CAnd cs) = fmap sconcat . sequence <$> mapM decomposeConstraint cs
+decomposeConstraint CTrue = return $ NE.singleton mempty
 decomposeConstraint (CAll ty) = do
   (vars, c) <- unbind ty
   let c' = substs (mkSkolems vars) c
-  (map . first . addSkolems) vars <$> decomposeConstraint c'
+  (NE.map . first . addSkolems) vars <$> decomposeConstraint c'
  where
   mkSkolems :: [Name Type] -> [(Name Type, Type)]
   mkSkolems = map (id &&& TySkolem)
-decomposeConstraint (COr cs) = concat <$> filterErrors (map decomposeConstraint cs)
+decomposeConstraint (COr cs) = sconcat <$> filterErrors (NE.map decomposeConstraint cs)
 
 decomposeQual ::
   Members '[Fresh, Error SolveError, Input TyDefCtx] r =>
@@ -878,6 +899,7 @@ data Rels = Rels
 -- | A RelMap associates each variable to its sets of base type and
 --   variable predecessors and successors in the constraint graph.
 newtype RelMap = RelMap {unRelMap :: Map (Name Type, Dir) Rels}
+  deriving (Show)
 
 instance Pretty RelMap where
   pretty (RelMap rm) = vcat (map prettyVar byVar)
@@ -950,6 +972,18 @@ lubBySort, glbBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name
 lubBySort vm rm = limBySort vm rm SuperTy
 glbBySort vm rm = limBySort vm rm SubTy
 
+allBySort :: TyVarInfoMap -> RelMap -> Dir -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
+allBySort vm rm dir ts s x =
+  isects
+    . map (\t -> S.fromList (dirtypesBySort vm rm dir t s x))
+    $ ts
+ where
+  isects = foldr1 S.intersection
+
+ubsBySort, lbsBySort :: TyVarInfoMap -> RelMap -> [BaseTy] -> Sort -> Set (Name Type) -> Set BaseTy
+ubsBySort vm rm = allBySort vm rm SuperTy
+lbsBySort vm rm = allBySort vm rm SubTy
+
 -- | From the constraint graph, build the sets of sub- and super- base
 --   types of each type variable, as well as the sets of sub- and
 --   supertype variables.  For each type variable x in turn, try to
@@ -964,11 +998,14 @@ glbBySort vm rm = limBySort vm rm SubTy
 --   predecessors in this case, since it seems nice to default to
 --   "simpler" types lower down in the subtyping chain.
 solveGraph ::
-  Members '[Fresh, Error SolveError, Output (Message ann)] r =>
+  Members '[Fresh, Error SolveError, Output (Message ann), State SolutionLimit] r =>
   TyVarInfoMap ->
   Graph UAtom ->
-  Sem r S
-solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
+  Sem r [S]
+solveGraph vm g = do
+  debug "Solving graph..."
+  debugPretty g
+  map (atomToTypeSubst . unifyWCC) <$> go topRelMap
  where
   unifyWCC :: Substitution BaseTy -> Substitution Atom
   unifyWCC s = compose (map mkEquateSubst wccVarGroups) @@ fmap ABase s
@@ -1030,35 +1067,37 @@ solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
     fromVar _ = error "Impossible! UB but uisVar."
 
   go ::
-    Members '[Fresh, Error SolveError, Output (Message ann)] r =>
+    Members '[Fresh, Output (Message ann), State SolutionLimit] r =>
     RelMap ->
-    Sem r (Substitution BaseTy)
-  go relMap@(RelMap rm) =
-    debugPretty relMap >> case as of
+    Sem r [Substitution BaseTy]
+  go relMap@(RelMap rm) = withSolutionLimit $ do
+    debugPretty relMap
+    case as of
       -- No variables left that have base type constraints.
-      [] -> return idS
+      [] -> do
+        -- Found a solution, decrement the counter.
+        countSolution
+        return [idS]
       -- Solve one variable at a time.  See below.
       (a : _) -> do
         debug $ "Solving for" <+> pretty' a
-        case solveVar a of
-          Nothing -> do
-            debug $ "Couldn't solve for" <+> pretty' a
-            throw NoUnify
-
-          -- If we solved for a, delete it from the maps, apply the
-          -- resulting substitution to the remainder (updating the
-          -- relMap appropriately), and recurse.  The substitution we
-          -- want will be the composition of the substitution for a
-          -- with the substitution generated by the recursive call.
-          --
-          -- Note we don't need to delete a from the TyVarInfoMap; we
-          -- never use the set of keys from the TyVarInfoMap for
-          -- anything (indeed, some variables might not be keys if
-          -- they have an empty sort), so it doesn't matter if old
-          -- variables hang around in it.
-          Just s -> do
-            debugPretty s
-            (@@ s) <$> go (substRel a (fromJust $ Subst.lookup (coerce a) s) relMap)
+        let ss = solveVar a
+        debugPretty ss
+
+        -- If we solved for a, delete it from the maps, apply the
+        -- resulting substitution to the remainder (updating the
+        -- relMap appropriately), and recurse.  The substitution we
+        -- want will be the composition of the substitution for a
+        -- with the substitution generated by the recursive call.
+        --
+        -- Note we don't need to delete a from the TyVarInfoMap; we
+        -- never use the set of keys from the TyVarInfoMap for
+        -- anything (indeed, some variables might not be keys if
+        -- they have an empty sort), so it doesn't matter if old
+        -- variables hang around in it.
+        ss' <- forM ss $ \s ->
+          map (@@ s) <$> go (substRel a (fromJust $ Subst.lookup (coerce a) s) relMap)
+        return (join ss')
    where
     -- NOTE we can't solve a bunch in parallel!  Might end up
     -- assigning them conflicting solutions if some depend on
@@ -1099,9 +1138,14 @@ solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
       [] -> filter ((/= topSort) . getSort vm) . map fst $ M.keys rm
       _ -> asBase
 
-    -- Solve for a variable, failing if it has no solution, otherwise returning
-    -- a substitution for it.
-    solveVar :: Name Type -> Maybe (Substitution BaseTy)
+    -- XXX the right way to do this is to keep track of the
+    -- polarity of each variable.  For variables that have only
+    -- one polarity we can pick the greatest or least solution as
+    -- appropriate.  For other variables, we have to return all of
+    -- them.
+
+    -- Solve for a variable, returning all possible substitutions.
+    solveVar :: Name Type -> [Substitution BaseTy]
     solveVar v =
       case ((v, SuperTy), (v, SubTy)) & over both (S.toList . baseRels . lkup "solveGraph.solveVar" rm) of
         -- No sub- or supertypes; the only way this can happen is
@@ -1122,24 +1166,22 @@ solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
         -- nontrivial sorts means that we are dealing with numeric
         -- types; so we can just call N a base subtype and go from
         -- there.
+        --
+        -- Hmm, no, this is wrong!  E.g. we could have a QCmp
+        -- constraint, in which case something like Char or Bool
+        -- could be OK...  In any case, this is really just to be
+        -- able to show users some sample types, it's not an issue
+        -- of soundness.  We don't (can't?) guarantee to return ALL possible types.
 
         ([], []) ->
-          if getSort vm v == S.fromList [QBool]
-            then Just (coerce v |-> B)
-            else -- Debug.trace (show v ++ " has no sub- or supertypes.  Assuming N as a subtype.")
-
-              (coerce v |->)
-                <$> lubBySort
-                  vm
-                  relMap
-                  [N]
-                  (getSort vm v)
-                  (varRels (lkup "solveVar none, rels" rm (v, SubTy)))
+          -- Debug.trace (show v ++ " has no sub- or supertypes.")
+          -- Pick some base type with an appropriate sort.
+          map (coerce v |->) $ filter (`hasSort` getSort vm v) [N, Z, F, Q, B, C]
         -- Only supertypes.  Just assign a to their inf, if one exists.
         (bsupers, []) ->
           -- Debug.trace (show v ++ " has only supertypes (" ++ show bsupers ++ ")") $
-          (coerce v |->)
-            <$> glbBySort
+          map (coerce v |->) . S.toList $
+            lbsBySort
               vm
               relMap
               bsupers
@@ -1148,35 +1190,23 @@ solveGraph vm g = atomToTypeSubst . unifyWCC <$> go topRelMap
         -- Only subtypes.  Just assign a to their sup.
         ([], bsubs) ->
           -- Debug.trace (show v ++ " has only subtypes (" ++ show bsubs ++ ")") $
-          -- Debug.trace ("sortmap: " ++ show vm) $
+          -- Debug.trace ("varmap: " ++ show vm) $
           -- Debug.trace ("relmap: " ++ show relMap) $
           -- Debug.trace ("sort for " ++ show v ++ ": " ++ show (getSort vm v)) $
           -- Debug.trace ("relvars: " ++ show (varRels (relMap ! (v,SubTy)))) $
-          (coerce v |->)
-            <$> lubBySort
+          map (coerce v |->) . S.toList $
+            ubsBySort
               vm
               relMap
               bsubs
               (getSort vm v)
               (varRels (lkup "solveVar bsubs, rels" rm (v, SubTy)))
         -- Both successors and predecessors.  Both must have a
-        -- valid bound, and the bounds must not overlap.  Assign a
-        -- to the sup of its predecessors.
-        (bsupers, bsubs) -> do
-          ub <-
-            glbBySort
-              vm
-              relMap
-              bsupers
-              (getSort vm v)
-              (varRels (rm ! (v, SuperTy)))
-          lb <-
-            lubBySort
-              vm
-              relMap
-              bsubs
-              (getSort vm v)
-              (varRels (rm ! (v, SubTy)))
-          case isSubB lb ub of
-            True -> Just (coerce v |-> lb)
-            False -> Nothing
+        -- valid bound, and the bounds must not overlap.
+        (bsupers, bsubs) ->
+          let mub = glbBySort vm relMap bsupers (getSort vm v) (varRels (rm ! (v, SuperTy)))
+              mlb = lubBySort vm relMap bsubs (getSort vm v) (varRels (rm ! (v, SubTy)))
+           in case (mlb, mub) of
+                (Just lb, Just ub) ->
+                  map (coerce v |->) (filter (`isSubB` ub) (supertypes lb))
+                _ -> []
diff --git a/src/Disco/Typecheck/Util.hs b/src/Disco/Typecheck/Util.hs
index 4db4ff42..2e4fd57d 100644
--- a/src/Disco/Typecheck/Util.hs
+++ b/src/Disco/Typecheck/Util.hs
@@ -8,25 +8,24 @@
 -- used during type checking.
 module Disco.Typecheck.Util where
 
-import Disco.Effects.Fresh
-import Polysemy
-import Polysemy.Error
-import Polysemy.Output
-import Polysemy.Reader
-import Polysemy.Writer
-import Unbound.Generics.LocallyNameless (Name, bind, string2Name)
-
+import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.Map as M
 import Data.Tuple (swap)
-import Prelude hiding (lookup)
-
 import Disco.AST.Surface
 import Disco.Context
+import Disco.Effects.Fresh
 import Disco.Messages
 import Disco.Names (ModuleName, QName)
 import Disco.Typecheck.Constraints
 import Disco.Typecheck.Solve
 import Disco.Types
+import Polysemy
+import Polysemy.Error
+import Polysemy.Output
+import Polysemy.Reader
+import Polysemy.Writer
+import Unbound.Generics.LocallyNameless (Name, bind, string2Name)
+import Prelude hiding (lookup)
 
 ------------------------------------------------------------
 -- Contexts
@@ -127,11 +126,11 @@ forAll nms = censor (CAll . bind nms)
 
 -- | Run two constraint-generating actions and combine the constraints
 --   via disjunction.
-cOr :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()
-cOr m1 m2 = do
+orElse :: Members '[Writer Constraint] r => Sem r () -> Sem r () -> Sem r ()
+orElse m1 m2 = do
   (c1, _) <- censor (const CTrue) (listen m1)
   (c2, _) <- censor (const CTrue) (listen m2)
-  constraint $ COr [c1, c2]
+  constraint $ COr (c1 :| [c2])
 
 -- | Run a computation that generates constraints, returning the
 --   generated 'Constraint' along with the output. Note that this
@@ -143,18 +142,20 @@ withConstraint :: Sem (Writer Constraint ': r) a -> Sem r (a, Constraint)
 withConstraint = fmap swap . runWriter
 
 -- | Run a computation and solve its generated constraint, returning
---   the resulting substitution (or failing with an error).  Note that
---   this locally dispatches the constraint writer effect.
+--   up to the requested number of possible resulting substitutions
+--   (or failing with an error).  Note that this locally dispatches
+--   the constraint writer and solution limit effects.
 solve ::
   Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r =>
+  Int ->
   Sem (Writer Constraint ': r) a ->
-  Sem r (a, S)
-solve m = do
+  Sem r (a, NonEmpty S)
+solve lim m = do
   (a, c) <- withConstraint m
-  res <- runSolve . inputToReader . solveConstraint $ c
+  res <- runSolve (SolutionLimit lim) . inputToReader . solveConstraint $ c
   case res of
     Left e -> throw (Unsolvable e)
-    Right s -> return (a, s)
+    Right ss -> return (a, ss)
 
 ------------------------------------------------------------
 -- Contexts
diff --git a/src/Disco/Util.hs b/src/Disco/Util.hs
index bf259f0b..6a120a2f 100644
--- a/src/Disco/Util.hs
+++ b/src/Disco/Util.hs
@@ -1,6 +1,4 @@
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
+{-# LANGUAGE ImportQualifiedPost #-}
 
 -- |
 -- Module      :  Disco.Util
@@ -12,7 +10,10 @@
 -- Miscellaneous utilities.
 module Disco.Util where
 
-import qualified Data.Map as M
+import Data.Bifunctor (bimap)
+import Data.List.NonEmpty (NonEmpty)
+import Data.List.NonEmpty qualified as NE
+import Data.Map qualified as M
 
 infixr 1 ==>
 
@@ -21,14 +22,43 @@ infixr 1 ==>
 (==>) :: a -> b -> (a, b)
 (==>) = (,)
 
+-- | Flipped variant of 'map'.
 for :: [a] -> (a -> b) -> [b]
 for = flip map
 
+-- | A variant of 'Map' indexing that throws a custom error message
+--   in case the key is not found, to help with debugging.
 (!) :: (Show k, Ord k) => M.Map k v -> k -> v
 m ! k = case M.lookup k m of
   Nothing -> error $ "key " ++ show k ++ " is not an element in the map"
   Just v -> v
 
+-- | Find the maximum of a list of positive numbers, yielding 0 in the
+--   case of an empty list.
 maximum0 :: (Num a, Ord a) => [a] -> a
 maximum0 [] = 0
 maximum0 xs = maximum xs
+
+-- | A variant of 'filter' that returns a @Maybe (NonEmpty a)@ instead
+--   of a regular list.
+filterNE :: (a -> Bool) -> NonEmpty a -> Maybe (NonEmpty a)
+filterNE p = NE.nonEmpty . NE.filter p
+
+-- | A variant of 'partition' that returns @Maybe (NonEmpty a)@s instead
+--   of regular lists.
+partitionNE :: (a -> Bool) -> NonEmpty a -> (Maybe (NonEmpty a), Maybe (NonEmpty a))
+partitionNE p as = (filterNE p as, filterNE (not . p) as)
+
+-- | A variant of 'partitionEithers' for nonempty lists.  If the
+--   result is Left, it means all the inputs were Left.  If the result
+--   is Right, we definitely have some Rights, and possibly some Lefts
+--   as well.  This properly encodes the fact that at least one result
+--   list must be nonempty.
+partitionEithersNE :: NonEmpty (Either a b) -> Either (NonEmpty a) ([a], NonEmpty b)
+partitionEithersNE = foldr1 combine . NE.map (bimap NE.singleton (([],) . NE.singleton))
+ where
+  combine :: Either (NonEmpty a) ([a], NonEmpty b) -> Either (NonEmpty a) ([a], NonEmpty b) -> Either (NonEmpty a) ([a], NonEmpty b)
+  combine (Left as1) (Left as2) = Left (NE.append as1 as2)
+  combine (Left as1) (Right (as2, bs)) = Right (NE.toList as1 ++ as2, bs)
+  combine (Right (as1, bs)) (Left as2) = Right (as1 ++ NE.toList as2, bs)
+  combine (Right (as1, bs1)) (Right (as2, bs2)) = Right (as1 ++ as2, NE.append bs1 bs2)
diff --git a/test/arith-basic-un/expected b/test/arith-basic-un/expected
index 9d5b374e..60216401 100644
--- a/test/arith-basic-un/expected
+++ b/test/arith-basic-un/expected
@@ -17,7 +17,9 @@
 -6
 Error: that number would not even fit in the universe!
 -9
+This expression has multiple possible types.  Some examples:
 -~ : ℤ → ℤ
+-~ : ℚ → ℚ
 -3 : ℤ
 -(3 : ℕ) : ℤ
 -(3 : 𝔽) : ℚ
diff --git a/test/containers-each/expected b/test/containers-each/expected
index 31dfd65c..05e7be6b 100644
--- a/test/containers-each/expected
+++ b/test/containers-each/expected
@@ -1,5 +1,23 @@
+This expression has multiple possible types.  Some examples:
 λxs. each(λx. x + 1, xs) : List(ℕ) → List(ℕ)
+λxs. each(λx. x + 1, xs) : Bag(ℕ) → Bag(ℕ)
+λxs. each(λx. x + 1, xs) : Set(ℕ) → Set(ℕ)
+λxs. each(λx. x + 1, xs) : List(ℤ) → List(ℤ)
+λxs. each(λx. x + 1, xs) : Bag(ℤ) → Bag(ℤ)
+λxs. each(λx. x + 1, xs) : Set(ℤ) → Set(ℤ)
+λxs. each(λx. x + 1, xs) : List(𝔽) → List(𝔽)
+λxs. each(λx. x + 1, xs) : Bag(𝔽) → Bag(𝔽)
+...
+This expression has multiple possible types.  Some examples:
 λxs. each(list, xs) : List(List(a)) → List(List(a))
+λxs. each(list, xs) : List(Bag(a)) → List(List(a))
+λxs. each(list, xs) : List(Set(a)) → List(List(a))
+λxs. each(list, xs) : Bag(List(a)) → Bag(List(a))
+λxs. each(list, xs) : Bag(Bag(a)) → Bag(List(a))
+λxs. each(list, xs) : Bag(Set(a)) → Bag(List(a))
+λxs. each(list, xs) : Set(List(a)) → Set(List(a))
+λxs. each(list, xs) : Set(Bag(a)) → Set(List(a))
+...
 each(λx. x + 1, [1, 2, 3]) : List(ℕ)
 each(λx. x + 1, ⟅1, 2, 3⟆) : Bag(ℕ)
 each(λx. x + 1, {1, 2, 3}) : Set(ℕ)
diff --git a/test/containers-reduce/expected b/test/containers-reduce/expected
index 9d072b8e..136e6c69 100644
--- a/test/containers-reduce/expected
+++ b/test/containers-reduce/expected
@@ -4,7 +4,10 @@ Running tests...
   dummy: OK
   setSize2: OK
 Loaded.
+This expression has multiple possible types.  Some examples:
 reduce : (a × a → a) × a × List(a) → a
+reduce : (a × a → a) × a × Bag(a) → a
+reduce : (a × a → a) × a × Set(a) → a
 reduce(~+~, 0, [1 .. 10]) : ℕ
 55
 60
diff --git a/test/graphs-basic/expected b/test/graphs-basic/expected
index e7156262..be762de6 100644
--- a/test/graphs-basic/expected
+++ b/test/graphs-basic/expected
@@ -1,4 +1,7 @@
+This expression has multiple possible types.  Some examples:
 emptyGraph : Graph(ℕ)
+emptyGraph : Graph(Bool)
+emptyGraph : Graph(Char)
 emptyGraph
 vertex(1) : Graph(ℕ)
 vertex(1)
diff --git a/test/map-basic/expected b/test/map-basic/expected
index 3e1d8f45..2ae02526 100644
--- a/test/map-basic/expected
+++ b/test/map-basic/expected
@@ -1,13 +1,31 @@
-map : Set(ℕ × a) → Map(ℕ, a)
-map({(1, 3), (4, 6)}) : Map(ℕ, ℕ)
+This expression has multiple possible types.  Some examples:
+map : Set(ℚ × a) → Map(ℚ, a)
+map : Set(Bool × a) → Map(Bool, a)
+map : Set(Char × a) → Map(Char, a)
+map({(1, 3), (4, 6)}) : Map(ℚ, ℕ)
 map({(1, 3), (4, 6)})
+This expression has multiple possible types.  Some examples:
 insert : ℕ × a × Map(ℕ, a) → Map(ℕ, a)
-map({}) : Map(ℕ, a)
+insert : ℤ × a × Map(ℤ, a) → Map(ℤ, a)
+insert : 𝔽 × a × Map(𝔽, a) → Map(𝔽, a)
+insert : ℚ × a × Map(ℚ, a) → Map(ℚ, a)
+insert : Bool × a × Map(Bool, a) → Map(Bool, a)
+insert : Char × a × Map(Char, a) → Map(Char, a)
+This expression has multiple possible types.  Some examples:
+map({}) : Map(ℚ, a)
+map({}) : Map(Bool, a)
+map({}) : Map(Char, a)
 map({})
 insert(1, 3, insert(4, 6, map({}))) : Map(ℕ, ℕ)
 map({(1, 3), (4, 6)})
 map({(1, 3)})
+This expression has multiple possible types.  Some examples:
 lookup : ℕ × Map(ℕ, a) → Unit + a
+lookup : ℤ × Map(ℤ, a) → Unit + a
+lookup : 𝔽 × Map(𝔽, a) → Unit + a
+lookup : ℚ × Map(ℚ, a) → Unit + a
+lookup : Bool × Map(Bool, a) → Unit + a
+lookup : Char × Map(Char, a) → Unit + a
 right(3)
 right(6)
 left(■)
diff --git a/test/poly-infer-sort/expected b/test/poly-infer-sort/expected
index a93a6fd8..08b8496c 100644
--- a/test/poly-infer-sort/expected
+++ b/test/poly-infer-sort/expected
@@ -1,11 +1,27 @@
+This expression has multiple possible types.  Some examples:
 let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x + x) : ℕ → ℕ
+let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x + x) : ℤ → ℤ
+let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x + x) : 𝔽 → 𝔽
+let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x + x) : ℚ → ℚ
+This expression has multiple possible types.  Some examples:
 let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x - x) : ℤ → ℤ
+let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x - x) : ℚ → ℚ
+This expression has multiple possible types.  Some examples:
 let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x / x) : 𝔽 → 𝔽
+let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. x / x) : ℚ → ℚ
 let f : (a → a) → a → a = λg. λx. g(g(x)) in f(λx. -x / x) : ℚ → ℚ
 λx. x : a → a
 λx. λy. x : a1 → a → a1
+This expression has multiple possible types.  Some examples:
 λx. λy. λz. x + y + z : ℕ → ℕ → ℕ → ℕ
+λx. λy. λz. x + y + z : ℤ → ℤ → ℤ → ℤ
+λx. λy. λz. x + y + z : ℕ → ℕ → 𝔽 → 𝔽
+λx. λy. λz. x + y + z : ℕ → 𝔽 → ℕ → 𝔽
+This expression has multiple possible types.  Some examples:
 λx. λy : ℕ. x - y : ℤ → ℕ → ℤ
-λw. λx : ℕ. λy. λz : 𝔽. w - x + y + z : ℚ → ℕ → ℚ → 𝔽 → ℚ
+λx. λy : ℕ. x - y : ℚ → ℕ → ℚ
+This expression has multiple possible types.  Some examples:
+λw. λx : ℕ. λy. λz : 𝔽. w - x + y + z : ℕ → ℕ → ℚ → 𝔽 → ℚ
+λw. λx : ℕ. λy. λz : 𝔽. w - x + y + z : ℤ → ℕ → ℤ → 𝔽 → ℚ
 Error: typechecking failed.
 https://disco-lang.readthedocs.io/en/latest/reference/typecheck-fail.html
diff --git a/test/poly-instantiate/expected b/test/poly-instantiate/expected
index addfd736..5ebdb681 100644
--- a/test/poly-instantiate/expected
+++ b/test/poly-instantiate/expected
@@ -3,10 +3,22 @@ Loaded.
 foldr : (a → r → r) → r → List(a) → r
 foldr(λx. λy. x) : a → List(a) → a
 foldr(λx. λy. y) : r → List(a) → r
+This expression has multiple possible types.  Some examples:
 foldr(λx. λy. x + 1) : ℕ → List(ℕ) → ℕ
+foldr(λx. λy. x + 1) : ℤ → List(ℤ) → ℤ
+foldr(λx. λy. x + 1) : 𝔽 → List(𝔽) → 𝔽
+foldr(λx. λy. x + 1) : ℚ → List(ℚ) → ℚ
+This expression has multiple possible types.  Some examples:
 foldr(λx. λy. y + 1) : ℕ → List(a) → ℕ
+foldr(λx. λy. y + 1) : ℤ → List(a) → ℤ
+foldr(λx. λy. y + 1) : 𝔽 → List(a) → 𝔽
+foldr(λx. λy. y + 1) : ℚ → List(a) → ℚ
 foldr(λx. λy. y + 1)(1) : List(a) → ℕ
 foldr(λx. λy. y + 1)(-1) : List(a) → ℤ
+This expression has multiple possible types.  Some examples:
 foldr(λx. λy. x)(F) : List(Bool) → Bool
-foldr(λx. λy. x + 1)(1 / 2) : List(ℕ) → 𝔽
-foldr(λx. λy. x - 1)(1 / 2) : List(ℤ) → ℚ
+foldr(λx. λy. x)(F) : List(Prop) → Prop
+This expression has multiple possible types.  Some examples:
+foldr(λx. λy. x + 1)(1 / 2) : List(𝔽) → 𝔽
+foldr(λx. λy. x + 1)(1 / 2) : List(ℤ) → ℚ
+foldr(λx. λy. x - 1)(1 / 2) : List(ℚ) → ℚ
diff --git a/test/repl-ann/expected b/test/repl-ann/expected
index 23bee77f..c51b02ed 100644
--- a/test/repl-ann/expected
+++ b/test/repl-ann/expected
@@ -1,3 +1,3 @@
 Loading num.disco...
 factor : ℕ → Bag(ℕ)
-(λx : ℤ. (λy : a. (~-~ : ℤ × ℤ → ℤ)((x : ℤ, 7 : ℤ) : ℤ × ℤ) : ℤ) : a3 → ℤ) : ℤ → a3 → ℤ
+(λx : ℕ. (λy : a. (~-~ : ℤ × ℤ → ℤ)((x : ℤ, 7 : ℤ) : ℤ × ℤ) : ℤ) : a3 → ℤ) : ℕ → a3 → ℤ
diff --git a/test/repl-doc/expected b/test/repl-doc/expected
index a48af845..1395cacd 100644
--- a/test/repl-doc/expected
+++ b/test/repl-doc/expected
@@ -16,14 +16,22 @@ f is a function.
 Some more documentation.
 
 No documentation found for 'x'.
+This expression has multiple possible types.  Some examples:
 ~+~ : ℕ × ℕ → ℕ
+~+~ : ℤ × ℤ → ℤ
+~+~ : 𝔽 × 𝔽 → 𝔽
+~+~ : ℚ × ℚ → ℚ
 precedence level 7, left associative
 
 The sum of two numbers, types, or graphs.
 
 https://disco-lang.readthedocs.io/en/latest/reference/addition.html
 
+This expression has multiple possible types.  Some examples:
 ~+~ : ℕ × ℕ → ℕ
+~+~ : ℤ × ℤ → ℤ
+~+~ : 𝔽 × 𝔽 → 𝔽
+~+~ : ℚ × ℚ → ℚ
 precedence level 7, left associative
 
 The sum of two numbers, types, or graphs.
diff --git a/test/table-function/expected b/test/table-function/expected
index 32e1b665..19082d27 100644
--- a/test/table-function/expected
+++ b/test/table-function/expected
@@ -48,6 +48,33 @@ T  T  T
  24  577
 ...
 
+  0   -1
+  1    0
+  2    3
+  3    8
+  4   15
+  5   24
+  6   35
+  7   48
+  8   63
+  9   80
+ 10   99
+ 11  120
+ 12  143
+ 13  168
+ 14  195
+ 15  224
+ 16  255
+ 17  288
+ 18  323
+ 19  360
+ 20  399
+ 21  440
+ 22  483
+ 23  528
+ 24  575
+...
+
   0   -1
   1    0
  -1    0
diff --git a/test/table-function/input b/test/table-function/input
index b26aa1bc..a385eb81 100644
--- a/test/table-function/input
+++ b/test/table-function/input
@@ -5,6 +5,7 @@
 :table /\
 :table \x. x^2 + 1
 :table \x. x^2 - 1
-:table \x. x + 1/2
+:table \x:Z. x^2 - 1
+:table \x:F. x + 1/2
 :table \x. reduce(~+~, 0, x)
 :table \x:Unit. unit
diff --git a/test/types-192/expected b/test/types-192/expected
index 02d6127c..37cec1c8 100644
--- a/test/types-192/expected
+++ b/test/types-192/expected
@@ -1 +1,4 @@
+This expression has multiple possible types.  Some examples:
 λx. λy. λz. x + y / z : 𝔽 → 𝔽 → 𝔽 → 𝔽
+λx. λy. λz. x + y / z : ℕ → ℕ → ℚ → ℚ
+λx. λy. λz. x + y / z : ℕ → ℤ → ℤ → ℚ
diff --git a/test/types-container/expected b/test/types-container/expected
index 0d275146..7b2839c9 100644
--- a/test/types-container/expected
+++ b/test/types-container/expected
@@ -7,6 +7,27 @@
 [3] : List(ℕ)
 {3} : Set(ℕ)
 ⟅3⟆ : Bag(ℕ)
+This expression has multiple possible types.  Some examples:
 list : List(a) → List(a)
+list : Bag(a) → List(a)
+list : Set(a) → List(a)
+This expression has multiple possible types.  Some examples:
 bag : List(ℕ) → Bag(ℕ)
+bag : Bag(ℕ) → Bag(ℕ)
+bag : Set(ℕ) → Bag(ℕ)
+bag : List(ℤ) → Bag(ℤ)
+bag : Bag(ℤ) → Bag(ℤ)
+bag : Set(ℤ) → Bag(ℤ)
+bag : List(𝔽) → Bag(𝔽)
+bag : Bag(𝔽) → Bag(𝔽)
+...
+This expression has multiple possible types.  Some examples:
 set : List(ℕ) → Set(ℕ)
+set : Bag(ℕ) → Set(ℕ)
+set : Set(ℕ) → Set(ℕ)
+set : List(ℤ) → Set(ℤ)
+set : Bag(ℤ) → Set(ℤ)
+set : Set(ℤ) → Set(ℤ)
+set : List(𝔽) → Set(𝔽)
+set : Bag(𝔽) → Set(𝔽)
+...
diff --git a/test/types-naked-ops/expected b/test/types-naked-ops/expected
index 311d8c65..9e49ff48 100644
--- a/test/types-naked-ops/expected
+++ b/test/types-naked-ops/expected
@@ -1,5 +1,17 @@
+This expression has multiple possible types.  Some examples:
 max : ℕ × ℕ → ℕ
+max : ℤ × ℤ → ℤ
+max : 𝔽 × 𝔽 → 𝔽
+max : ℚ × ℚ → ℚ
+max : Bool × Bool → Bool
+max : Char × Char → Char
 ~! : ℕ → ℕ
+This expression has multiple possible types.  Some examples:
+~mod~ : ℕ × ℕ → ℕ
 ~mod~ : ℤ × ℤ → ℤ
+This expression has multiple possible types.  Some examples:
 ~+~ : ℕ × ℕ → ℕ
+~+~ : ℤ × ℤ → ℤ
+~+~ : 𝔽 × 𝔽 → 𝔽
+~+~ : ℚ × ℚ → ℚ
 not~ : Bool → Bool
diff --git a/test/types-standalone-ops/expected b/test/types-standalone-ops/expected
index a1ec4246..ba8cc43d 100644
--- a/test/types-standalone-ops/expected
+++ b/test/types-standalone-ops/expected
@@ -1,4 +1,6 @@
 ~/\~ : Bool × Bool → Bool
 F /\ T : Bool
+This expression has multiple possible types.  Some examples:
 λx. x /\ T : Bool → Bool
+λx. x /\ T : Prop → Prop
 let f : (Bool × Bool → Bool) → Bool = λg. g(T, F) in f(~/\~) : Bool