From 629a6f0db01ab6646d3a75839a29466c6d114ac9 Mon Sep 17 00:00:00 2001
From: matheus <matheus.de.alcantara@gmail.com>
Date: Sat, 19 Oct 2019 10:09:32 -0300
Subject: [PATCH] Quick Look Impredicativity (#203)

This lets us infer /some/ uses of impredicative types.
---
 amuletml.cabal                                |   1 +
 src/Syntax/Pretty.hs                          |   5 +
 src/Types/Infer.hs                            |  62 +----
 src/Types/Infer.hs-boot                       |   4 +
 src/Types/Infer/App.hs                        | 224 ++++++++++++++++++
 src/Types/Infer/Builtin.hs                    |  19 +-
 src/Types/Infer/Class.hs                      |   2 +-
 src/Types/Kinds.hs                            |   8 +-
 src/Types/Unify.hs                            |  28 ++-
 tests/lua/default-method.lua                  |   2 +-
 tests/lua/list.lua                            |   2 +-
 tests/lua/monoid.lua                          |  18 +-
 tests/lua/nested_match.lua                    |   6 +-
 tests/lua/op_apply.lua                        |   2 +-
 tests/lua/stream-zip.lua                      |  12 +-
 tests/lua/values_occ.lua                      |   6 +-
 tests/types/class/constraint-category.out     |   6 +-
 tests/types/class/default02-fail.out          |   2 +-
 tests/types/class/fundep01.out                |   4 +-
 tests/types/class/fundep02.out                |   4 +-
 tests/types/class/row-cons-fail.out           |   2 +-
 tests/types/gadt/dict02-fail.out              |  14 +-
 tests/types/gadt/fail_term.out                |   4 +-
 tests/types/gadt/fin.out                      |   2 +-
 tests/types/idioms.out                        |   2 +-
 tests/types/nasty_cycle.out                   |   8 +-
 tests/types/rankn/impredicative01-fail.out    |   6 -
 ...tive01-fail.ml => impredicative01-pass.ml} |   0
 tests/types/rankn/impredicative01-pass.out    |   3 +
 tests/types/rankn/ql-impredicative.ml         |   4 +
 tests/types/rankn/ql-impredicative.out        |   3 +
 tests/types/rankn/ql-impredicative02.ml       |  13 +
 tests/types/rankn/ql-impredicative02.out      |   5 +
 tests/types/rankn/ql-impredicative03.ml       |   6 +
 tests/types/rankn/ql-impredicative03.out      |   4 +
 tests/types/rankn/ql-impredicative04.ml       |   7 +
 tests/types/rankn/ql-impredicative04.out      |   6 +
 tests/types/rankn/ql-impredicative05.ml       |   6 +
 tests/types/rankn/ql-impredicative05.out      |   8 +
 tests/types/rankn/ql-impredicative06.ml       |  10 +
 tests/types/rankn/ql-impredicative06.out      |   8 +
 tests/types/rankn/req-fail.out                |   2 +-
 42 files changed, 414 insertions(+), 126 deletions(-)
 create mode 100644 src/Types/Infer/App.hs
 delete mode 100644 tests/types/rankn/impredicative01-fail.out
 rename tests/types/rankn/{impredicative01-fail.ml => impredicative01-pass.ml} (100%)
 create mode 100644 tests/types/rankn/impredicative01-pass.out
 create mode 100644 tests/types/rankn/ql-impredicative.ml
 create mode 100644 tests/types/rankn/ql-impredicative.out
 create mode 100644 tests/types/rankn/ql-impredicative02.ml
 create mode 100644 tests/types/rankn/ql-impredicative02.out
 create mode 100644 tests/types/rankn/ql-impredicative03.ml
 create mode 100644 tests/types/rankn/ql-impredicative03.out
 create mode 100644 tests/types/rankn/ql-impredicative04.ml
 create mode 100644 tests/types/rankn/ql-impredicative04.out
 create mode 100644 tests/types/rankn/ql-impredicative05.ml
 create mode 100644 tests/types/rankn/ql-impredicative05.out
 create mode 100644 tests/types/rankn/ql-impredicative06.ml
 create mode 100644 tests/types/rankn/ql-impredicative06.out

diff --git a/amuletml.cabal b/amuletml.cabal
index 1285344b6..1c1d00ae6 100644
--- a/amuletml.cabal
+++ b/amuletml.cabal
@@ -241,6 +241,7 @@ library
                      , Types.Kinds
                      , Types.Unify
                      , Types.Infer.Let
+                     , Types.Infer.App
                      , Types.Wellformed
                      , Types.Unify.Magic
                      , Types.Infer.Class
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index ec5b931a7..265877a23 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -130,7 +130,12 @@ prettyType (TyPi x t) = uncurry prettyQuantifiers . second reverse $ unwind t [x
   sameAs Anon{} Anon{} = True
   sameAs Implicit{} Implicit{} = True
   sameAs _ _ = False
+
 prettyType (TyApp (TyApp (TyCon v) l) r) | isOpName (displayS (pretty v)) = prettyType (TyOperator l v r)
+-- Hack for the guarded unification magic type: \/
+prettyType (TyApp (TyCon v) x) | show (pretty v) == mempty = displayType x
+-- This is really gross
+
 prettyType (TyApp x e) = parenTyFun x (displayType x) <+> parenTyArg e (displayType e)
 prettyType (TyRows p rows) = enclose (lbrace <> space) (space <> rbrace) $
   pretty p <+> soperator pipe <+> hsep (punctuate comma (displayRows rows))
diff --git a/src/Types/Infer.hs b/src/Types/Infer.hs
index 20c5aa20d..3b9bed3e8 100644
--- a/src/Types/Infer.hs
+++ b/src/Types/Infer.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE FlexibleContexts, TupleSections, ScopedTypeVariables,
-   ViewPatterns, LambdaCase, TypeFamilies, CPP #-}
+   ViewPatterns, LambdaCase, TypeFamilies, CPP, UndecidableInstances #-}
 module Types.Infer
   ( inferProgram, inferExpr
   , closeOver
 
   , infer, check, solveEx
+  , instantiateTc, infer'
   ) where
 
 import Prelude
@@ -39,6 +40,7 @@ import Types.Infer.Function
 import Types.Infer.Pattern
 import Types.Infer.Builtin
 import Types.Infer.Class
+import Types.Infer.App
 import Types.Infer.Let
 import Types.Kinds
 import Types.Unify
@@ -114,7 +116,7 @@ check (Let ns b an) t = do
         pure (Let ns b (an, t))
 
 check ex@(Fun pat e an) ty = do
-  (dom, cod, _) <- quantifier (becauseExp ex) ty
+  (dom, cod, _) <- quantifier (becauseExp ex) (/= Req) ty
   let domain = _tyBinderType dom
 
   (p, tau, vs, cs, is) <- inferParameter pat
@@ -167,6 +169,9 @@ check ex@(Ascription e ty an) goal = do
   c <- subsumes (becauseExp ex) ty goal
   pure (ExprWrapper c e (an, goal))
 
+check ex@App{} expected = fst <$> inferApps ex (pure expected)
+check ex@Vta{} expected = fst <$> inferApps ex (pure expected)
+
 check (Parens e _) ty = check e ty
 
 check AccessSection{} tau =
@@ -242,22 +247,15 @@ infer ex@(Ascription e ty an) = do
   e <- check e ty
   pure (Ascription (correct ty e) ty (an, ty), ty)
 
-infer ex@(BinOp l o r a) = do
-  (o, ty) <- infer o
-
-  ~(Anon lt, c1, k1) <- quantifier (becauseExp ex) ty
-  ~(Anon rt, c2, k2) <- quantifier (becauseExp ex) c1
-
-  (l, r) <- (,) <$> check l lt <*> check r rt
-  pure (App (k2 (App (k1 o) l (a, c1))) r (a, c2), c2)
+infer (BinOp l o r a) = inferApps (App (App o l a) r a) Nothing
 
 infer ex@App{} = do
-  (ex, ty) <- inferApp ex
+  (ex, ty) <- inferApps ex Nothing
   (k, ty) <- secondA expandType =<< instantiateTc (becauseExp ex) ty
   pure (k ex, ty)
 
 infer ex@Vta{} = do
-  (ex, ty) <- inferApp ex
+  (ex, ty) <- inferApps ex Nothing
   (k, ty) <- secondA expandType =<< instantiateTc (becauseExp ex) ty
   pure (k ex, ty)
 
@@ -326,42 +324,10 @@ infer' (VarRef k a) = do
   (cont, old, ty) <- lookupTy' Weak k
   ty <- expandType ty
   pure (fromMaybe id cont (VarRef k (a, old)), ty)
-infer' ex@App{} = inferApp ex
-infer' ex@Vta{} = inferApp ex
+infer' ex@App{} = inferApps ex Nothing
+infer' ex@Vta{} = inferApps ex Nothing
 infer' x = infer x
 
-inferApp :: MonadInfer Typed m => Expr Desugared -> m (Expr Typed, Type Typed)
-inferApp ex@(App f x a) = do
-  (f, ot) <- infer' f
-  (dom, c, k) <- quantifier (becauseExp ex) ot
-  case dom of
-    Anon d -> do
-      x <- check x d
-      pure (App (k f) x (a, c), c)
-    Invisible _ _ Req -> do
-      (_, t) <- infer x
-      b <- freshTV
-      confesses (NotEqual ot (TyArr t b))
-    Invisible{} -> error "invalid invisible quantification in App"
-    Implicit{} -> error "invalid invisible quantification in App"
-
-inferApp ex@(Vta f x a) = do
-  (f, ot) <- infer' f
-  (dom, c) <- retcons (addBlame (becauseExp ex)) $
-    firstForall x ot
-  case dom of
-    Invisible v kind r | r /= Infer{} -> do
-      x <- case kind of
-        Just k -> checkAgainstKind (becauseExp ex) x k
-        Nothing -> resolveKind (becauseExp ex) x
-      let ty = apply (Map.singleton v x) c
-      pure (ExprWrapper (TypeApp x) f (a, ty), ty)
-    Invisible{} -> error "inferred forall should always be eliminated"
-    Implicit{} -> error "invalid implicit quantification in Vta"
-    Anon{} -> error "invalid arrow type in Vta"
-
-inferApp _ = error "not an application"
-
 inferRows :: MonadInfer Typed m
           => [Field Desugared]
           -> m [(Field Typed, (T.Text, Type Typed))]
@@ -539,10 +505,6 @@ closeOverStrat r _ e t =
       confesses (ValueRestriction r t vars)
     annotateKind r t
 
-firstForall :: MonadInfer Typed m => Type Desugared -> Type Typed -> m (TyBinder Typed, Type Typed)
-firstForall _ (TyPi x@Invisible{} k) = pure (x, k)
-firstForall a e = confesses (CanNotVta e a)
-
 instantiateTc :: MonadInfer Typed m
               => SomeReason
               -> Type Typed
diff --git a/src/Types/Infer.hs-boot b/src/Types/Infer.hs-boot
index 69d2bda53..f0e594948 100644
--- a/src/Types/Infer.hs-boot
+++ b/src/Types/Infer.hs-boot
@@ -5,6 +5,7 @@ module Types.Infer
   , closeOver
 
   , infer, check, solveEx
+  , infer', instantiateTc
   ) where
 
 import Prelude hiding (lookup)
@@ -26,5 +27,8 @@ inferProgram :: MonadNamey m => Env -> [Toplevel Desugared] -> m (These [TypeErr
 check :: forall m. MonadInfer Typed m => Expr Desugared -> Type Typed -> m (Expr Typed)
 
 infer :: MonadInfer Typed m => Expr Desugared -> m (Expr Typed, Type Typed)
+infer' :: MonadInfer Typed m => Expr Desugared -> m (Expr Typed, Type Typed)
+
+instantiateTc :: MonadInfer Typed m => SomeReason -> Type Typed -> m (Expr Typed -> Expr Typed, Type Typed)
 
 solveEx :: TySyms -> Subst Typed -> Map.Map (Var Typed) (Wrapper Typed) -> Expr Typed -> Expr Typed
diff --git a/src/Types/Infer/App.hs b/src/Types/Infer/App.hs
new file mode 100644
index 000000000..97ba6750b
--- /dev/null
+++ b/src/Types/Infer/App.hs
@@ -0,0 +1,224 @@
+{-# LANGUAGE FlexibleContexts, TupleSections, ScopedTypeVariables,
+   TypeFamilies, CPP, StandaloneDeriving, UndecidableInstances #-}
+module Types.Infer.App (inferApps) where
+
+import Prelude
+
+import qualified Data.Map.Strict as Map
+import qualified Data.Text as T
+import Data.Traversable
+import Data.Foldable
+import Data.Spanned
+import Data.Reason
+import Data.Triple
+import Data.Maybe
+
+import Control.Monad.Infer
+import Control.Lens
+
+import Syntax.Subst
+import Syntax.Var
+import Syntax
+
+import Types.Infer.Builtin
+import {-# SOURCE #-} Types.Infer
+import Types.Kinds
+import Types.Unify
+
+import Text.Pretty.Semantic
+
+
+#ifdef TRACE_TC
+import Debug.Trace
+#endif
+
+-- | Infer an application, supporting "Quick Look" impredicativity: We
+-- consider all of the arguments to a function application (or
+-- operator) together, then do two passes over them:
+--
+--  * The first pass is what we call a 'quick look'. Here, we try to
+--  infer polymorphic type instantiations for some of the function's
+--  arguments. This pass only considers "simple" arguments: Variables
+--  (for now).
+--
+--  * The second pass is the real use of 'checks' that we've always done
+--  for arguments.
+inferApps :: forall m. MonadInfer Typed m => Expr Desugared -> Maybe (Type Typed) -> m (Expr Typed, Type Typed)
+inferApps exp expected =
+  do
+    let ((ExprArg function, _):arguments) = reverse $ spine exp
+    (function, function_t) <- infer' function
+    function_t <- refresh function_t
+
+#ifdef TRACE_TC
+    traceM ("function type: " ++ displayS (pretty function_t))
+#endif
+
+    ((ql_sub, quantifiers), cs) <-
+      censor (const mempty) . listen $
+        quickLook function_t =<< for arguments (\a@(x, y) -> (x, y,) <$> inferQL a)
+
+    quantifiers <- pure (applyQ ql_sub quantifiers)
+
+    let fake_ty_con = TyCon (TgInternal T.empty)
+    for_ (Map.toList ql_sub) $ \(var, tau) ->
+      -- Here we need these to be guarded, so they need to be in the RHS
+      -- of a type application. Since we don't have a suitable type, we
+      -- use an internal TyCon with an invisible name. (Evil!)
+      unify (becauseExp exp) (TyApp fake_ty_con (TyVar var)) (TyApp fake_ty_con tau)
+
+    tell cs
+
+    r_ql_sub <- case expected of
+      Just tau@(TyApps (TyCon _) (_:_)) | result@(TyApps (TyCon _) (_:_)) <- getQuantR quantifiers -> do
+-- Pushing down the result type into the quick look substitution
+-- is only sound if both are /guarded/. Do note that missing a
+-- substitution here isn't unsound, it'll just lead to wonky inference.
+        _ <- subsumes (becauseExp exp) result (apply ql_sub tau)
+        pure $ fromMaybe mempty (unifyPure result tau)
+      _ -> pure mempty
+
+#ifdef TRACE_TC
+    traceM ("Quick Look results: " ++ show (pretty <$> (ql_sub <> r_ql_sub), pretty quantifiers))
+#endif
+
+    (arg_ks, result) <-
+      checkArguments arguments (applyQ r_ql_sub quantifiers)
+
+#ifdef TRACE_TC
+    traceM ("resulting type: " ++ displayS (pretty result))
+#endif
+
+    wrap <- case expected of
+      Just tau -> do
+#ifdef TRACE_TC
+        traceM ("QL expected result: " ++ displayS (pretty tau))
+#endif
+        wrap <- subsumes (becauseExp exp) result tau
+        pure $ \ex -> ExprWrapper wrap ex (annotation ex, tau)
+      Nothing -> pure id
+
+    pure (wrap (foldr (.) id (reverse arg_ks) function), result)
+  where
+    spine ex@(App fn arg _) =
+      let sp = spine fn
+       in (ExprArg arg, BecauseOf ex):sp
+    spine ex@(Vta fn arg _) =
+      let sp = spine fn
+       in (TypeArg arg, BecauseOf ex):sp
+    spine ex = [(ExprArg ex, BecauseOf ex)]
+
+    checkArguments ((ExprArg arg, _):as) (Quant tau dom cod inst_cont qs) =
+      case dom of
+        Anon dom -> do
+          x <- check arg dom
+
+          let cont ex = App ex x (annotation ex <> annotation x, cod)
+
+          (conts, result) <- checkArguments as qs
+          pure (inst_cont:cont:conts, result)
+        Invisible _ _ Req -> do
+          (_, t) <- infer arg
+          b <- freshTV
+          confesses (NotEqual tau (TyArr t b))
+        _ -> error "checkArguments ExprArg: impossible quantifier"
+
+    checkArguments ((TypeArg arg, reason):as) (Quant tau dom cod inst_cont qs) =
+      case dom of
+        Invisible v kind r | r /= Infer{} -> do
+          arg <- case kind of
+            Just k -> checkAgainstKind reason arg k
+            Nothing -> resolveKind reason arg
+
+          let ty = apply (Map.singleton v arg) cod
+              cont ex = ExprWrapper (TypeApp arg) ex (annotation ex <> annotation reason, ty)
+
+          (conts, result) <- checkArguments as qs
+          pure (inst_cont:cont:conts, result)
+        _ -> confesses (ArisingFrom (CanNotVta tau arg) reason)
+
+    checkArguments [] Quant{} = error "arity mismatch. impossible in checkArguments"
+
+    checkArguments _ (Result tau) = pure ([], tau)
+
+quickLook :: MonadInfer Typed m
+          => Type Typed
+          -> [(Arg Desugared, SomeReason, Maybe (Type Typed))]
+          -> m ( Subst Typed
+               , Quantifiers Typed )
+quickLook t ((ExprArg _, reason, ql_t):args) = do
+  (dom, cod, wrap) <- quantifier reason (/= Req) t
+  case dom of
+    Anon dom -> do
+      let sub =
+            case ql_t of
+              Just ql_t -> fromMaybe mempty (unifyPure dom ql_t)
+              _ -> mempty
+      (rest_sub, qs) <- quickLook (apply sub cod) args
+      pure (sub `compose` rest_sub, Quant t (Anon (apply sub dom)) (apply sub cod) wrap qs)
+    _ -> do
+      (sub, qs) <- quickLook cod args
+      pure (sub, Quant t dom cod wrap qs)
+quickLook t ((TypeArg tau, reason, _):args) = do
+  tau <- liftType reason tau
+  (dom, cod, wrap) <- quantifier reason (== Infer) t
+  case dom of
+    Invisible v _ _ -> do
+      let sub = Map.singleton v tau
+      (rest_sub, qs) <- quickLook (apply sub cod) args
+      pure (sub `compose` rest_sub, Quant t dom (apply sub cod) wrap qs)
+    _ -> do
+      (sub, qs) <- quickLook cod args
+      pure (sub, Quant t dom cod wrap qs)
+quickLook tau [] = pure (mempty, Result tau)
+
+inferQL :: MonadInfer Typed m => (Arg Desugared, SomeReason) -> m (Maybe (Type Typed))
+inferQL (arg, reason) = case arg of
+  ExprArg a -> inferQL_ex a
+  TypeArg tau -> pure <$> liftType reason tau
+
+inferQL_ex :: MonadInfer Typed m => Expr Desugared -> m (Maybe (Type Typed))
+inferQL_ex ex@(VarRef x _) = do
+  (_, _, (new, _)) <- third3A (discharge ex) =<< lookupTy' Strong x
+  (_, tau) <- censor (const mempty) $ instantiateTc (BecauseOf ex) new
+  if hasPoly tau
+     then pure (pure tau)
+     else pure Nothing
+inferQL_ex (Literal l _) = pure (pure (litTy l))
+inferQL_ex ex@(Ascription _ t _) = pure <$> liftType (BecauseOf ex) t
+inferQL_ex _ = pure Nothing
+
+data Arg p = ExprArg (Expr p) | TypeArg (Type p)
+deriving instance (Show (Var p), Show (Ann p)) => Show (Arg p)
+
+instance Pretty (Var p) => Pretty (Arg p) where
+  pretty (ExprArg e) = pretty e
+  pretty (TypeArg t) = char '@' <> pretty t
+
+data Quantifiers p = Quant (Type p) (TyBinder p) (Type p) (Expr p -> Expr p) (Quantifiers p) | Result (Type p)
+
+instance Pretty (Var p) => Pretty (Quantifiers p) where
+  pretty (Result t) = pretty t
+  pretty (Quant _ b _ _ qs) = pretty b <+> pretty qs
+
+applyQ :: Subst Typed -> Quantifiers Typed -> Quantifiers Typed
+applyQ sub (Quant tau quant cod wrap qs) = Quant tau (apply sub quant) cod wrap (applyQ sub qs)
+applyQ sub (Result t) = Result (apply sub t)
+
+getQuantR :: Quantifiers p -> Type p
+getQuantR (Quant _ _ _ _ qs) = getQuantR qs
+getQuantR (Result t) = t
+
+refresh :: MonadNamey m => Type Typed -> m (Type Typed)
+refresh (TyPi (Invisible v k r) t) = do
+  let nn (TgName t _) = t
+      nn (TgInternal t) = t
+  new_v <- genNameFrom (nn v)
+  let sub = Map.singleton v (TyVar new_v)
+  TyPi (Invisible new_v k r) <$> refresh (apply sub t)
+refresh t = pure t
+
+hasPoly :: Type Typed -> Bool
+hasPoly = any isForall . universe where
+  isForall (TyPi Invisible{} _) = True
+  isForall _ = False
diff --git a/src/Types/Infer/Builtin.hs b/src/Types/Infer/Builtin.hs
index 17e75be1a..a14588d2b 100644
--- a/src/Types/Infer/Builtin.hs
+++ b/src/Types/Infer/Builtin.hs
@@ -114,34 +114,35 @@ decompose r p t =
 -- instantiating 'TyForall's and discharging 'Implicit' binders.
 quantifier :: MonadInfer Typed m
            => SomeReason
+           -> (Specificity -> Bool) -- The quantifiers we can skip over.
            -> Type Typed
            -> m (TyBinder Typed, Type Typed, Expr Typed -> Expr Typed)
 
-quantifier r (TyPi (Invisible v _ req) rest) | req /= Req = do
+quantifier r pred (TyPi (Invisible v _ req) rest) | pred req = do
   var <- refreshTV v
   let map = Map.singleton v var
       exp ex | an <- annotation ex =
         ExprWrapper (TypeApp var) ex (an, apply map rest)
-  (a, b, k) <- quantifier r (apply map rest)
+  (a, b, k) <- quantifier r pred (apply map rest)
   pure (a, b, k . exp)
 
-quantifier r ty@TyWithConstraints{} = do
+quantifier r pred ty@TyWithConstraints{} = do
   (rest, k) <- discharge (Const r) ty
-  (a, b, k') <- quantifier r rest
+  (a, b, k') <- quantifier r pred rest
   pure (a, b, k' . k)
 
-quantifier r wty@(TyPi (Implicit tau) sigma) = do
+quantifier r pred wty@(TyPi (Implicit tau) sigma) = do
   x <- genName
   i <- view classes
   tell (Seq.singleton (ConImplicit r i x tau))
 
-  (dom, cod, k) <- quantifier r sigma
+  (dom, cod, k) <- quantifier r pred sigma
   let wrap ex = ExprWrapper (WrapVar x) (ExprWrapper (TypeAsc wty) ex (annotation ex, wty)) (annotation ex, sigma)
   pure (dom, cod, k . wrap)
 
-quantifier _ (TyPi x b) = pure (x, b, id)
-quantifier _ (TyApp (TyApp (TyCon n) l) r) | n == tyArrowName = pure (Anon l, r, id)
-quantifier r t = do
+quantifier _ _ (TyPi x b) = pure (x, b, id)
+quantifier _ _ (TyApp (TyApp (TyCon n) l) r) | n == tyArrowName = pure (Anon l, r, id)
+quantifier r _ t = do
   (a, b) <- (,) <$> freshTV <*> freshTV
   k <- subsumes r t (TyPi (Anon a) b)
   pure (Anon a, b, \x -> ExprWrapper k x (annotation x, TyPi (Anon a) b))
diff --git a/src/Types/Infer/Class.hs b/src/Types/Infer/Class.hs
index 6c001f5d2..9d67a9b18 100644
--- a/src/Types/Infer/Class.hs
+++ b/src/Types/Infer/Class.hs
@@ -611,7 +611,7 @@ guardOrphans inst inScope [] tycons
   | otherwise = dictates (OrphanInstance inst (Set.fromList (Map.elems tycons) Set.\\ inScope))
 
 guardOrphans inst inScope fundeps tycons = for_ fundeps $ \(_, det, _) -> do
-  let tc = tycons `Map.withoutKeys` (Set.fromList det)
+  let tc = tycons `Map.withoutKeys` Set.fromList det
   unless (any (`Set.member` inScope) (Map.elems tc)) $
     dictates (OrphanInstance inst (Set.fromList (Map.elems tycons) Set.\\ inScope))
 
diff --git a/src/Types/Kinds.hs b/src/Types/Kinds.hs
index 2796f2ac7..2c3116fbb 100644
--- a/src/Types/Kinds.hs
+++ b/src/Types/Kinds.hs
@@ -285,8 +285,8 @@ inferKind (TyOperator left op right) = do
     Just k ->
       view _3 <$> instantiate Strong Expression k
 
-  ~(Anon lt, c1, _) <- quantifier reason ty
-  ~(Anon rt, c2, _) <- quantifier reason c1
+  ~(Anon lt, c1, _) <- quantifier reason (/= Req) ty
+  ~(Anon rt, c2, _) <- quantifier reason (/= Req) c1
   left <- checkKind left lt
   right <- checkKind right rt
   pure (TyOperator left op right, c2)
@@ -322,7 +322,7 @@ inferKind t@TyApp{} | TyCon v:xs <- appsView t = do
 
   reason <- get
   let checkOne arg kind = do
-        (dom, cod, _) <- quantifier reason kind
+        (dom, cod, _) <- quantifier reason (/= Req) kind
         case dom of
           Anon d -> do
             arg <- checkKind arg d
@@ -350,7 +350,7 @@ inferKind t@TyApp{} | TyCon v:xs <- appsView t = do
 
 inferKind (TyApp f x) = do
   reason <- get
-  (f, (dom, c, _)) <- secondA (quantifier reason) =<< inferKind f
+  (f, (dom, c, _)) <- secondA (quantifier reason (/= Req)) =<< inferKind f
 
   case dom of
     Anon d -> do
diff --git a/src/Types/Unify.hs b/src/Types/Unify.hs
index d96676193..5072de4ba 100644
--- a/src/Types/Unify.hs
+++ b/src/Types/Unify.hs
@@ -82,6 +82,7 @@ data SolveScope
                , _don'tTouch :: Set.Set (Var Typed)
                , _depth :: [Type Typed]
                , _solveInfo :: SolverInfo
+               , _guarded :: Bool
                }
   deriving (Eq, Show, Ord)
 
@@ -142,7 +143,7 @@ runSolve :: MonadNamey m
          -> m ([Constraint Typed], SolveState)
 runSolve skol info s x = runReaderT (runStateT (execWriterT act) s) emptyScope where
   act = (,) <$> genName <*> x
-  emptyScope = SolveScope skol mempty [] info
+  emptyScope = SolveScope skol mempty [] info False
 
 getSolveInfo :: MonadReader Env m => m SolverInfo
 getSolveInfo = do
@@ -189,7 +190,7 @@ doSolve (ConUnify because scope v a b :<| xs) = do
   sub <- use solveTySubst
   scope <- pure (apply sub scope)
 
-  traceM (displayS (keyword "[W]:" <+> pretty because <+> pretty (ConUnify because scope v (apply sub a) (apply sub b))))
+  traceM (displayS (keyword "[W]:" <+> pretty (ConUnify because scope v (apply sub a) (apply sub b))))
 
   solveFuel .= SOLVER_FUEL
 
@@ -206,7 +207,7 @@ doSolve (ConUnify because scope v a b :<| xs) = do
 doSolve (ConSubsume because scope v a b :<| xs) = do
   sub <- use solveTySubst
 
-  traceM (displayS (pretty because <+> pretty (ConSubsume because scope v (apply sub a) (apply sub b))))
+  traceM (displayS (pretty (ConSubsume because scope v (apply sub a) (apply sub b))))
   let a' = apply sub a
   sub <- use solveTySubst
 
@@ -460,8 +461,6 @@ bind scope var ty
   | TyVar var == ty = pure (ReflCo ty)
   -- /\ Var-var deletion
   | TyWildcard (Just (TyVar v)) <- ty, v == var = pure (ReflCo ty)
-  -- /\ Var-wildcard deletion (same as above, but with an indirection)
-  | TyPi (Invisible _ _ r) _ <- ty, r /= Req = confesses (Impredicative var ty)
   -- /\ Predicativity checking
   | otherwise = do
       env <- use solveTySubst
@@ -690,7 +689,8 @@ unify scope ta@(TyApps (TyCon v) xs@(_:_)) b = do
 
       TyApps f ys@(_:_) | length xs == length ys -> rethrow ta b $ do
         heads <- unify scope (TyCon v) f
-        tails <- traverse (uncurry (unify scope)) (zip xs ys)
+        tails <- polyInstSafe $
+          traverse (uncurry (unify scope)) (zip xs ys)
         pure (foldl AppCo heads tails)
 
       TyApps f ys@(_:_) | length ys < length xs -> rethrow ta b $ do
@@ -703,9 +703,10 @@ unify scope ta@(TyApps (TyCon v) xs@(_:_)) b = do
             xs_a = take (xs_l - ys_l) xs
             xs_b = drop (xs_l - ys_l) xs
 
-        heads <- unify scope (TyApps (TyCon v) xs_a) f
-        tails <- traverse (uncurry (unify scope)) (zip xs_b ys)
-        pure (foldl AppCo heads tails)
+        polyInstSafe $ do
+          heads <- unify scope (TyApps (TyCon v) xs_a) f
+          tails <- traverse (uncurry (unify scope)) (zip xs_b ys)
+          pure (foldl AppCo heads tails)
 
       _ -> do
         doWork (unequal ta b)
@@ -977,7 +978,7 @@ subsumes' r scope ot@(TyTuple a b) nt@(TyTuple a' b') = do -- {{{
   pure (WrapFn (MkWrapCont cont "tuple re-packing")) -- }}}
 
 subsumes' _ s a@(TyApp lazy _) b@(TyApp lazy' _)
-  | lazy == lazy', lazy' == tyLazy = probablyCast <$> unify s a b
+  | lazy == lazy', lazy' == tyLazy = probablyCast <$> polyInstSafe (unify s a b)
 
 subsumes' r scope (TyApp lazy ty') ty | lazy == tyLazy, lazySubOk ty' ty = do
   co <- subsumes' r scope ty' ty
@@ -1250,6 +1251,13 @@ prettyConcrete _ = True
 concreteUnderOne :: Type Typed -> Bool
 concreteUnderOne t = all prettyConcrete (appsView t)
 
+isPoly :: Type p -> Bool
+isPoly (TyPi (Invisible _ _ r) _) = r /= Req
+isPoly _ = False
+
+polyInstSafe :: MonadReader SolveScope m => m a -> m a
+polyInstSafe = local (guarded .~ True)
+
 firstBlame, secondBlame :: SomeReason -> SomeReason
 firstBlame (It'sThis (BecauseOfExpr (Tuple (x:_) _) _)) = becauseExp x
 firstBlame x = x
diff --git a/tests/lua/default-method.lua b/tests/lua/default-method.lua
index db1662f47..da25b85ca 100644
--- a/tests/lua/default-method.lua
+++ b/tests/lua/default-method.lua
@@ -1,4 +1,4 @@
 do
   local use = print
-  use(function(fu) return "tail" .. "()" end)
+  use(function(fw) return "tail" .. "()" end)
 end
diff --git a/tests/lua/list.lua b/tests/lua/list.lua
index eb11c09e6..a927d0410 100644
--- a/tests/lua/list.lua
+++ b/tests/lua/list.lua
@@ -31,7 +31,7 @@ do
     local b = x + 1
     local function w(xss0)
       if xss0.__tag == "Cons" then
-        return { { _1 = { _1 = x, _2 = b }, _2 = w(xss0[1]._2) }, __tag = "Cons" }
+        return { { _2 = w(xss0[1]._2), _1 = { _1 = x, _2 = b } }, __tag = "Cons" }
       end
       return s(xs)
     end
diff --git a/tests/lua/monoid.lua b/tests/lua/monoid.lua
index 996cf246e..a7711c098 100644
--- a/tests/lua/monoid.lua
+++ b/tests/lua/monoid.lua
@@ -2,27 +2,27 @@ do
   local Nil = { __tag = "Nil" }
   local tostring = tostring
   local writeln = print
-  local function _dollardApplicativeakf(tmp)
+  local function _dollardApplicativeako(tmp)
     return {
-      ["<*>"] = function(tmp0) return function(tmp1) return tmp["×"](tmp0)(tmp1) end end,
       pure = function(tmp0) return tmp.zero end,
+      ["<*>"] = function(tmp0) return function(tmp1) return tmp["×"](tmp0)(tmp1) end end,
       ["Applicative$kb"] = function(tmp0) return function(tmp1) return tmp1 end end
     }
   end
   local function _colon_colon(x)
     return function(y) return { { _1 = x, _2 = y }, __tag = "Cons" } end
   end
-  local function _dollarshow(bay, x)
+  local function _dollarshow(bam, x)
     if x.__tag == "Nil" then return "Nil" end
     local tmp = x[1]
-    return bay(tmp._1) .. " :: " .. _dollarshow(bay, tmp._2)
+    return bam(tmp._1) .. " :: " .. _dollarshow(bam, tmp._2)
   end
-  local function _dollartraverse(brd, tmp, k, x)
+  local function _dollartraverse(brr, tmp, k, x)
     if x.__tag == "Nil" then return tmp.pure(Nil) end
     local tmp0 = x[1]
     return tmp["<*>"](tmp["Applicative$kb"](_colon_colon)(k(tmp0._1)))(_dollartraverse(nil, tmp, k, tmp0._2))
   end
-  local function _dollar_d7(bwk, x, ys)
+  local function _dollar_d7(bxc, x, ys)
     if x.__tag == "Nil" then return ys end
     local tmp = x[1]
     return { { _2 = _dollar_d7(nil, tmp._2, ys), _1 = tmp._1 }, __tag = "Cons" }
@@ -30,9 +30,9 @@ do
   local tmp = { _1 = 1, _2 = nil }
   writeln(_dollarshow(function(x)
     return tostring(x)
-  end, _dollartraverse(nil, _dollardApplicativeakf({
-    ["×"] = function(x) return function(ys) return _dollar_d7(nil, x, ys) end end,
-    zero = Nil
+  end, _dollartraverse(nil, _dollardApplicativeako({
+    zero = Nil,
+    ["×"] = function(x) return function(ys) return _dollar_d7(nil, x, ys) end end
   }), function(tmp0) return { { _1 = tmp0._1, _2 = Nil }, __tag = "Cons" } end, {
     {
       _1 = tmp,
diff --git a/tests/lua/nested_match.lua b/tests/lua/nested_match.lua
index 7b9523f85..d6f931343 100644
--- a/tests/lua/nested_match.lua
+++ b/tests/lua/nested_match.lua
@@ -7,9 +7,9 @@ do
     local tmp2 = ys[1]
     local tmp3, tmp4 = tmp2._1, tmp2._2
     local tmp0, tmp1 = tmp._1, tmp._2
-    if tmp3 ~= 0 then return { { _1 = f(tmp0)(tmp3), _2 = zip(f, tmp1, tmp4) }, __tag = "Cons" } end
-    if tmp0 == 0 then return { { _1 = 3, _2 = Nil }, __tag = "Cons" } end
-    return { { _1 = f(tmp0)(0), _2 = zip(f, tmp1, tmp4) }, __tag = "Cons" }
+    if tmp0 ~= 0 then return { { _1 = f(tmp0)(tmp3), _2 = zip(f, tmp1, tmp4) }, __tag = "Cons" } end
+    if tmp3 == 0 then return { { _1 = 3, _2 = Nil }, __tag = "Cons" } end
+    return { { _1 = f(0)(tmp3), _2 = zip(f, tmp1, tmp4) }, __tag = "Cons" }
   end
   local function zip0(f) return function(xs) return function(ys) return zip(f, xs, ys) end end end
   (nil)(zip0)
diff --git a/tests/lua/op_apply.lua b/tests/lua/op_apply.lua
index f9e435114..923526391 100644
--- a/tests/lua/op_apply.lua
+++ b/tests/lua/op_apply.lua
@@ -2,9 +2,9 @@ do
   local function _at_at(tmp) return function(tmp0) return tmp(tmp0) end end
   local function tmp(x) return x end
   (nil)({
+    lsec = function(tmp0) return tmp(tmp0) end,
     op = _at_at,
     rsec = function(r) return r(2) end,
-    lsec = function(tmp0) return tmp(tmp0) end,
     app = 2
   })
 end
diff --git a/tests/lua/stream-zip.lua b/tests/lua/stream-zip.lua
index e2e33eaa9..f22a5477b 100644
--- a/tests/lua/stream-zip.lua
+++ b/tests/lua/stream-zip.lua
@@ -25,27 +25,27 @@ do
               return Skip({ _2 = { _1 = sb, _2 = None }, _1 = tmp5[1] })
             elseif tmp5.__tag == "Yield" then
               local tmp6 = tmp5[1]
-              return Skip({ _2 = { _1 = sb, _2 = Some(tmp6._1) }, _1 = tmp6._2 })
+              return Skip({ _1 = tmp6._2, _2 = { _1 = sb, _2 = Some(tmp6._1) } })
             elseif tmp5.__tag == "Done" then
               return Done
             end
           else
-            local tmp5 = g(sb)
             local x0 = x[1]
+            local tmp5 = g(sb)
             if tmp5.__tag == "Skip" then
-              return Skip({ _1 = sa, _2 = { _1 = tmp5[1], _2 = Some(x0) } })
+              return Skip({ _1 = sa, _2 = { _2 = Some(x0), _1 = tmp5[1] } })
             elseif tmp5.__tag == "Yield" then
               local tmp6 = tmp5[1]
               return Yield({
-                _2 = { _1 = sa, _2 = { _2 = None, _1 = tmp6._2 } },
-                _1 = { _1 = x0, _2 = tmp6._1 }
+                _1 = { _1 = x0, _2 = tmp6._1 },
+                _2 = { _1 = sa, _2 = { _2 = None, _1 = tmp6._2 } }
               })
             elseif tmp5.__tag == "Done" then
               return Done
             end
           end
         end,
-        _2 = { _1 = start, _2 = { _2 = None, _1 = tmp2._2 } }
+        _2 = { _1 = start, _2 = { _1 = tmp2._2, _2 = None } }
       })
     end
   end
diff --git a/tests/lua/values_occ.lua b/tests/lua/values_occ.lua
index 038ac9a89..d1671e755 100644
--- a/tests/lua/values_occ.lua
+++ b/tests/lua/values_occ.lua
@@ -6,12 +6,12 @@ do
     local tmp = xs[1]
     local go = tmp._1
     return Stream({
-      _2 = tmp._2,
       _1 = function(st)
         local tmp0 = go(st)
         local x = tmp0._1
-        return { _1 = x * x, _2 = tmp0._2 }
-      end
+        return { _2 = tmp0._2, _1 = x * x }
+      end,
+      _2 = tmp._2
     })
   end
   print(to_string(sum_squares))
diff --git a/tests/types/class/constraint-category.out b/tests/types/class/constraint-category.out
index e9cbb9e8f..c6df7b556 100644
--- a/tests/types/class/constraint-category.out
+++ b/tests/types/class/constraint-category.out
@@ -22,7 +22,7 @@ initial : Spec{'a : constraint}. :- impossible 'a
 terminal : Spec{'a : constraint}. :- 'a trivial
 map_dict : Spec{'a : constraint}. Spec{'b : constraint}. :- 'a 'b -> dict 'a -> dict 'b
 unmap_dict : Spec{'a : constraint}. Spec{'b : constraint}. (dict 'a -> dict 'b) -> :- 'a 'b
-:~: : Infer{'bas : type}. 'bas -> 'bas -> type
-Refl : Infer{'bax : type}. Infer{'bas : type}. Spec{'b : 'bax}. Spec{'a : 'bas}. ('b ~ 'a) ⊃ :~: 'a 'b
+:~: : Infer{'a : type}. 'a -> 'a -> type
+Refl : Infer{'bce : type}. Infer{'a : type}. Spec{'b : 'bce}. Spec{'a : 'a}. ('b ~ 'a) ⊃ :~: 'a 'b
 eq_dict : Infer{'a : type}. Spec{'b : 'a}. Spec{'c : 'a}. :~: 'b 'c -> dict (~ 'b 'c)
-dict_eq : Infer{'bas : type}. Spec{'a : 'bas}. Spec{'b : 'bas}. dict (~ 'a 'b) -> :~: 'a 'b
+dict_eq : Infer{'a : type}. Spec{'b : 'a}. Spec{'c : 'a}. dict (~ 'b 'c) -> :~: 'b 'c
diff --git a/tests/types/class/default02-fail.out b/tests/types/class/default02-fail.out
index a655656ba..8d849584e 100644
--- a/tests/types/class/default02-fail.out
+++ b/tests/types/class/default02-fail.out
@@ -6,7 +6,7 @@ default02-fail.ml[14:8 ..14:15]: error
   • Note: default method implementations should always be applicable,
     and thus can not have any extra constraints
 
-  Arising in the this expression
+  Arising in the the expression
    │ 
 14 │     if x `eq` x then
    │        ^^^^^^^^
diff --git a/tests/types/class/fundep01.out b/tests/types/class/fundep01.out
index 0617c69a8..5eb2fa5bf 100644
--- a/tests/types/class/fundep01.out
+++ b/tests/types/class/fundep01.out
@@ -4,8 +4,8 @@ k1 : Infer{'a : type}. type -> 'a -> type
 K1 : Spec{'a : type}. Spec{'x : 'a}. 'a -> k1 'a 'x
 foo : type
 Foo : int -> foo
-gshow : Infer{'ia : type}. ('ia -> type) -> constraint
-gshow : Spec{'f : 'ia -> type}. gshow 'f => Infer{'ia : type}. Spec{'x : 'ia}. 'f 'x -> string
+gshow : Infer{'id : type}. ('id -> type) -> constraint
+gshow : Spec{'f : 'id -> type}. gshow 'f => Infer{'id : type}. Spec{'x : 'id}. 'f 'x -> string
 show : type -> constraint
 show : Spec{'a : type}. show 'a => 'a -> string
 genericShow : Infer{'a : type}. Infer{'f : 'ad -> type}. gshow 'f => generic 'a 'f => 'a -> string
diff --git a/tests/types/class/fundep02.out b/tests/types/class/fundep02.out
index d0ee9855a..e707a0735 100644
--- a/tests/types/class/fundep02.out
+++ b/tests/types/class/fundep02.out
@@ -10,8 +10,8 @@ AddS : Infer{'il : type}. Infer{'im : type}. Spec{'a : 'il}. Spec{'c : 'im}. Spe
 add : nat -> nat -> nat -> constraint
 ev : Spec{'a : nat}. Spec{'b : nat}. Spec{'c : nat}. add 'a 'b 'c => add_ev 'a 'b 'c
 vect : nat -> type -> type
-Nil : Infer{'wy : type}. Spec{'n : 'wy}. Spec{'a : type}. ('n ~ Z) ⊃ vect 'n 'a
-Cons : Infer{'yg : type}. Spec{'n : 'yg}. Spec{'a : type}. Spec{'n : nat}. ('n ~ S 'n) ⊃ ('a * vect 'n 'a) -> vect 'n 'a
+Nil : Infer{'xl : type}. Spec{'n : 'xl}. Spec{'a : type}. ('n ~ Z) ⊃ vect 'n 'a
+Cons : Infer{'yt : type}. Spec{'n : 'yt}. Spec{'a : type}. Spec{'n : nat}. ('n ~ S 'n) ⊃ ('a * vect 'n 'a) -> vect 'n 'a
 append_with : Spec{'k : nat}. Spec{'l : nat}. Spec{'n : nat}. Spec{'a : type}. add_ev 'n 'k 'l -> vect 'n 'a -> vect 'k 'a -> vect 'l 'a
 append : Infer{'k : nat}. Infer{'l : nat}. Infer{'n : nat}. Infer{'a : type}. add 'n 'k 'l => vect 'n 'a -> vect 'k 'a -> vect 'l 'a
 :: : Infer{'a : type}. Infer{'n : nat}. 'a -> vect 'n 'a -> vect (S 'n) 'a
diff --git a/tests/types/class/row-cons-fail.out b/tests/types/class/row-cons-fail.out
index 3a3739982..fdc0681e1 100644
--- a/tests/types/class/row-cons-fail.out
+++ b/tests/types/class/row-cons-fail.out
@@ -1,5 +1,5 @@
 row-cons-fail.ml[1:9 ..1:39]: error
-  No instance for row_cons 'record "y" 'type { x : int } arising in this expression
+  No instance for row_cons 'record "y" 'type { x : int } arising in the expression
   │ 
 1 │ let x = Amc.restrict_row @"y" { x = 1 }
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/types/gadt/dict02-fail.out b/tests/types/gadt/dict02-fail.out
index b03509bff..dd2f81a3c 100644
--- a/tests/types/gadt/dict02-fail.out
+++ b/tests/types/gadt/dict02-fail.out
@@ -1,6 +1,12 @@
-dict02-fail.ml[17:25 ..17:26]: error
+dict02-fail.ml[17:17 ..17:22]: error
    │ 
 17 │ let x = with_d (bar ()) () (fun x -> show x)
-   │                         ^^
-  Couldn't match actual type unit
-    with the type expected by the context, int
+   │                 ^^^^^^
+  Couldn't match actual type dict (show int)
+    with the type expected by the context, dict ('c unit)
+dict02-fail.ml[17:17 ..17:22]: error
+   │ 
+17 │ let x = with_d (bar ()) () (fun x -> show x)
+   │                 ^^^^^^
+  Couldn't match actual type dict (show int)
+    with the type expected by the context, dict ('c unit)
diff --git a/tests/types/gadt/fail_term.out b/tests/types/gadt/fail_term.out
index 68df22798..7f0377fe2 100644
--- a/tests/types/gadt/fail_term.out
+++ b/tests/types/gadt/fail_term.out
@@ -1,12 +1,12 @@
 fail_term.ml[16:3 ..16:30]: error
-  No instance for 'a -> 'b -> 'b ~ 'b -> 'y -> 'b arising in this expression
+  No instance for 'a -> 'b -> 'b ~ 'b -> 'y -> 'b arising in the expression
    │ 
 16 │   Lam (Lam (Var (There Here)))
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   • Because:
   Could not match the rigid type variable 'b with the type 'a
 
-  • Arising in this expression
+  • Arising in the expression
    │ 
 16 │   Lam (Lam (Var (There Here)))
    │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/types/gadt/fin.out b/tests/types/gadt/fin.out
index ee80fe1cd..854f75226 100644
--- a/tests/types/gadt/fin.out
+++ b/tests/types/gadt/fin.out
@@ -1,5 +1,5 @@
 fin.ml[11:14 ..11:18]: error
-  No instance for 'n ~ S (S 'k) arising in this expression
+  No instance for 'n ~ S (S 'k) arising in the expression
    │ 
 11 │   | SS SZ -> FS FZ
    │              ^^^^^
diff --git a/tests/types/idioms.out b/tests/types/idioms.out
index 1af298b75..657519219 100644
--- a/tests/types/idioms.out
+++ b/tests/types/idioms.out
@@ -1,3 +1,3 @@
 pure : Infer{'a : type}. 'a -> list 'a
 <*> : Infer{'a : type}. Infer{'b : type}. list ('b -> 'a) -> list 'b -> list 'a
-cartesian : Infer{'b : type}. Infer{'a : type}. list 'a -> list 'b -> list ('a * 'b)
+cartesian : Infer{'a : type}. Infer{'b : type}. list 'a -> list 'b -> list ('a * 'b)
diff --git a/tests/types/nasty_cycle.out b/tests/types/nasty_cycle.out
index a8bb6d6da..e374d3f29 100644
--- a/tests/types/nasty_cycle.out
+++ b/tests/types/nasty_cycle.out
@@ -1,4 +1,4 @@
-nasty_cycle.ml[19:20 ..19:25]: error
+nasty_cycle.ml[19:25 ..19:25]: error
   Could not match the rigid type variable 's with the type S 's
 
   Where the type variable s is an existential,
@@ -8,9 +8,9 @@ nasty_cycle.ml[19:20 ..19:25]: error
   • Arising in the this expression
    │ 
 19 │       | Right p -> Left p
-   │                    ^^^^^^
+   │                         ^
 nasty_cycle.ml[18:26 ..18:32]: error
-  No instance for S 'n ~ S (S 's) arising in this expression
+  No instance for S 'n ~ S (S 's) arising in the expression
    │ 
 18 │       | Left p -> Right (Even2 p)
    │                          ^^^^^^^
@@ -21,7 +21,7 @@ nasty_cycle.ml[18:26 ..18:32]: error
   bound by the constructor SS, which has type
      forall 'n 's. snat 's -> snat (S 's)
 
-  • Arising in the this expression
+  • Arising in the the expression
    │ 
 18 │       | Left p -> Right (Even2 p)
    │                          ^^^^^^^
diff --git a/tests/types/rankn/impredicative01-fail.out b/tests/types/rankn/impredicative01-fail.out
deleted file mode 100644
index 3e871e8e4..000000000
--- a/tests/types/rankn/impredicative01-fail.out
+++ /dev/null
@@ -1,6 +0,0 @@
-impredicative01-fail.ml[6:38 ..6:52]: error
-  │ 
-6 │ let foo : id (forall 'a. 'a -> 'a) = Id (fun x -> x)
-  │                                      ^^^^^^^^^^^^^^^
-  Couldn't match actual type id ('ah -> 'ah)
-    with the type expected by the context, id (forall 'a. 'a -> 'a)
diff --git a/tests/types/rankn/impredicative01-fail.ml b/tests/types/rankn/impredicative01-pass.ml
similarity index 100%
rename from tests/types/rankn/impredicative01-fail.ml
rename to tests/types/rankn/impredicative01-pass.ml
diff --git a/tests/types/rankn/impredicative01-pass.out b/tests/types/rankn/impredicative01-pass.out
new file mode 100644
index 000000000..24f1c0ff7
--- /dev/null
+++ b/tests/types/rankn/impredicative01-pass.out
@@ -0,0 +1,3 @@
+id : type -> type
+Id : Spec{'a : type}. 'a -> id 'a
+foo : id (Spec{'a : type}. 'a -> 'a)
diff --git a/tests/types/rankn/ql-impredicative.ml b/tests/types/rankn/ql-impredicative.ml
new file mode 100644
index 000000000..994815434
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative.ml
@@ -0,0 +1,4 @@
+let x :: xs = Cons (x, xs)
+
+let id_list : list (forall 'a. 'a -> 'a) = []
+let ids = (fun x -> x) :: id_list
diff --git a/tests/types/rankn/ql-impredicative.out b/tests/types/rankn/ql-impredicative.out
new file mode 100644
index 000000000..684a1066a
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative.out
@@ -0,0 +1,3 @@
+:: : Infer{'a : type}. 'a -> list 'a -> list 'a
+id_list : list (Spec{'a : type}. 'a -> 'a)
+ids : list (Spec{'a : type}. 'a -> 'a)
diff --git a/tests/types/rankn/ql-impredicative02.ml b/tests/types/rankn/ql-impredicative02.ml
new file mode 100644
index 000000000..c946f07bc
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative02.ml
@@ -0,0 +1,13 @@
+let x :: xs = Cons (x, xs)
+
+let ids : list (forall 'a. 'a -> 'a) =
+  let empty : list (forall 'a. 'a -> 'a) = []
+  (fun x -> x) :: empty
+
+external val (+) : int -> int -> int = ""
+
+let length = function
+  | [] -> 0
+  | Cons (_, xs) -> 1 + length xs
+
+let x = length ids
diff --git a/tests/types/rankn/ql-impredicative02.out b/tests/types/rankn/ql-impredicative02.out
new file mode 100644
index 000000000..b0eaff01e
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative02.out
@@ -0,0 +1,5 @@
+:: : Infer{'a : type}. 'a -> list 'a -> list 'a
+ids : list (Spec{'a : type}. 'a -> 'a)
++ : int -> int -> int
+length : Infer{'a : type}. list 'a -> int
+x : int
diff --git a/tests/types/rankn/ql-impredicative03.ml b/tests/types/rankn/ql-impredicative03.ml
new file mode 100644
index 000000000..a15aad3f0
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative03.ml
@@ -0,0 +1,6 @@
+let map f xs = [ f x | with x <- xs ]
+let poly (f : forall 'a. 'a -> 'a) = (f 123, f true)
+
+let single x = [x]
+
+let x = map poly (single (fun x -> x))
diff --git a/tests/types/rankn/ql-impredicative03.out b/tests/types/rankn/ql-impredicative03.out
new file mode 100644
index 000000000..1a469e2ce
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative03.out
@@ -0,0 +1,4 @@
+map : Infer{'a : type}. Infer{'b : type}. ('b -> 'a) -> list 'b -> list 'a
+poly : (Spec{'a : type}. 'a -> 'a) -> int * bool
+single : Infer{'a : type}. 'a -> list 'a
+x : list (int * bool)
diff --git a/tests/types/rankn/ql-impredicative04.ml b/tests/types/rankn/ql-impredicative04.ml
new file mode 100644
index 000000000..004907384
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative04.ml
@@ -0,0 +1,7 @@
+let x |> f = f x
+let f :@ x = f x
+let poly (f : forall 'a. 'a -> 'a) = (f 123, f true)
+let id x = x
+
+let a = id |> poly
+let b = poly :@ id
diff --git a/tests/types/rankn/ql-impredicative04.out b/tests/types/rankn/ql-impredicative04.out
new file mode 100644
index 000000000..5e5f1eb00
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative04.out
@@ -0,0 +1,6 @@
+|> : Infer{'a : type}. Infer{'b : type}. 'a -> ('a -> 'b) -> 'b
+:@ : Infer{'a : type}. Infer{'b : type}. ('a -> 'b) -> 'a -> 'b
+poly : (Spec{'a : type}. 'a -> 'a) -> int * bool
+id : Infer{'a : type}. 'a -> 'a
+a : int * bool
+b : int * bool
diff --git a/tests/types/rankn/ql-impredicative05.ml b/tests/types/rankn/ql-impredicative05.ml
new file mode 100644
index 000000000..2beed6c53
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative05.ml
@@ -0,0 +1,6 @@
+let auto' = fun (x : forall 'a. 'a -> 'a) -> x
+let choose (x : 'a) (_ : 'a) = x
+
+let id x = x
+
+let t = choose id auto'
diff --git a/tests/types/rankn/ql-impredicative05.out b/tests/types/rankn/ql-impredicative05.out
new file mode 100644
index 000000000..32747dc7c
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative05.out
@@ -0,0 +1,8 @@
+ql-impredicative05.ml[6:16 ..6:17]: error
+  │ 
+6 │ let t = choose id auto'
+  │                ^^
+  Couldn't match actual type 'a -> 'a
+    with the type expected by the context, forall 'b. 'b -> 'b
+
+  • Did you forget some of the arguments to a function?
diff --git a/tests/types/rankn/ql-impredicative06.ml b/tests/types/rankn/ql-impredicative06.ml
new file mode 100644
index 000000000..47474cc30
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative06.ml
@@ -0,0 +1,10 @@
+let auto (x : forall 'a. 'a -> 'a) : forall 'b. 'b -> 'b = x
+let choose (x : 'a) (_ : 'a) = x
+
+let id x = x
+
+(* This /would/ work, as in the paper, but amulet deeply instantiates
+ * the type of auto to be the same as auto' in ql-impredicative05.ml.
+ *
+ * Darn. *)
+let t = choose id auto
diff --git a/tests/types/rankn/ql-impredicative06.out b/tests/types/rankn/ql-impredicative06.out
new file mode 100644
index 000000000..9ea6430c2
--- /dev/null
+++ b/tests/types/rankn/ql-impredicative06.out
@@ -0,0 +1,8 @@
+ql-impredicative06.ml[10:16 ..10:17]: error
+   │ 
+10 │ let t = choose id auto
+   │                ^^
+  Couldn't match actual type 'b -> 'b
+    with the type expected by the context, forall 'a. 'a -> 'a
+
+  • Did you forget some of the arguments to a function?
diff --git a/tests/types/rankn/req-fail.out b/tests/types/rankn/req-fail.out
index 55f990a48..bfb8ac775 100644
--- a/tests/types/rankn/req-fail.out
+++ b/tests/types/rankn/req-fail.out
@@ -3,6 +3,6 @@ req-fail.ml[3:5 ..3:5]: error
 3 │ let _ = foo 123
   │     ^
   Couldn't match actual type forall 'a -> 'a -> unit
-    with the type expected by the context, int -> 'j
+    with the type expected by the context, int -> 'k
 
   • Did you apply a function to too many arguments?