diff --git a/libs/base/Deriving/Functor.idr b/libs/base/Deriving/Functor.idr
new file mode 100644
index 000000000..43899e2ce
--- /dev/null
+++ b/libs/base/Deriving/Functor.idr
@@ -0,0 +1,491 @@
+||| Deriving functor instances using reflection
+||| You can for instance define:
+||| ```
+||| data Tree a = Leaf a | Node (Tree a) (Tree a)
+||| treeFunctor : Functor Tree
+||| treeFunctor = %runElab derive
+||| ```
+
+module Deriving.Functor
+
+import public Control.Monad.Either
+import public Control.Monad.State
+import public Data.Maybe
+import public Decidable.Equality
+import public Language.Reflection
+
+%language ElabReflection
+%default total
+
+freshName : List Name -> String -> String
+freshName ns a = assert_total $ go (basicNames ns) Nothing where
+
+  basicNames : List Name -> List String
+  basicNames = mapMaybe $ \ nm => case dropNS nm of
+    UN (Basic str) => Just str
+    _ => Nothing
+
+  covering
+  go : List String -> Maybe Nat -> String
+  go ns mi =
+    let nm = a ++ maybe "" show mi in
+    ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
+
+
+------------------------------------------------------------------------------
+-- Errors
+
+||| Possible errors for the functor-deriving machinery.
+public export
+data Error : Type where
+  NegativeOccurence : Name -> TTImp -> Error
+  NotAnApplication : TTImp -> Error
+  NotAFunctor : TTImp -> Error
+  NotABifunctor : TTImp -> Error
+  NotAFunctorInItsLastArg : TTImp -> Error
+  UnsupportedType : TTImp -> Error
+  InvalidGoal : Error
+  ConfusingReturnType : Error
+  -- Contextual information
+  WhenCheckingConstructor : Name -> Error -> Error
+  WhenCheckingArg : TTImp -> Error -> Error
+
+export
+Show Error where
+  show = joinBy "\n" . go [<] where
+
+    go : SnocList String -> Error -> List String
+    go acc (NegativeOccurence a ty) = acc <>> ["Negative occurence of \{show a} in \{show ty}"]
+    go acc (NotAnApplication s) = acc <>> ["The type \{show s} is not an application"]
+    go acc (NotAFunctor s) = acc <>> ["Couldn't find a `Functor' instance for the type constructor \{show s}"]
+    go acc (NotABifunctor s) = acc <>> ["Couldn't find a `Bifunctor' instance for the type constructor \{show s}"]
+    go acc (NotAFunctorInItsLastArg s) = acc <>> ["Not a functor in its last argument \{show s}"]
+    go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
+    go acc InvalidGoal = acc <>> ["Expected a goal of the form `Functor f`"]
+    go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
+    go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
+    go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
+
+------------------------------------------------------------------------------
+-- Preliminaries: satisfying an interface
+--
+-- In order to derive Functor for `data Tree a = Node (List (Tree a))`, we need
+-- to make sure that `Functor List` already exists. This is done using the following
+-- convenience functions.
+
+record IsType where
+  constructor MkIsType
+  typeConstructor  : Name
+  parameterNames   : List (Name, Nat)
+  dataConstructors : List (Name, TTImp)
+
+wording : NameType -> String
+wording Bound = "a bound variable"
+wording Func = "a function name"
+wording (DataCon tag arity) = "a data constructor"
+wording (TyCon tag arity) = "a type constructor"
+
+isTypeCon : Elaboration m => Name -> m (List (Name, TTImp))
+isTypeCon ty = do
+    [(_, MkNameInfo (TyCon _ _))] <- getInfo ty
+      | [] => fail "\{show ty} out of scope"
+      | [(_, MkNameInfo nt)] => fail "\{show ty} is \{wording nt} rather than a type constructor"
+      | _ => fail "\{show ty} is ambiguous"
+    cs <- getCons ty
+    for cs $ \ n => do
+      [(_, ty)] <- getType n
+         | _ => fail "\{show n} is ambiguous"
+      pure (n, ty)
+
+isType : Elaboration m => TTImp -> m IsType
+isType = go Z where
+
+  go : Nat -> TTImp -> m IsType
+  go idx (IVar _ n) = MkIsType n [] <$> isTypeCon n
+  go idx (IApp _ t (IVar _ nm)) = case nm of
+    -- Unqualified: that's a local variable
+    UN (Basic _) => { parameterNames $= ((nm, idx) ::) } <$> go (S idx) t
+    _ => go (S idx) t
+  go idx t = fail "Expected a type constructor, got: \{show t}"
+
+record Parameters where
+  constructor MkParameters
+  asFunctors : List Nat
+  asBifunctors : List Nat
+
+initParameters : Parameters
+initParameters = MkParameters [] []
+
+withParams : FC -> Parameters -> List (Name, Nat) -> TTImp -> TTImp
+withParams fc params nms t = go nms where
+
+  addConstraint : Bool -> Name -> Name -> TTImp -> TTImp
+  addConstraint False _ _ = id
+  addConstraint True cst nm =
+     let ty = IApp fc (IVar fc cst) (IVar fc nm) in
+     IPi fc MW AutoImplicit Nothing ty
+
+  go : List (Name, Nat) -> TTImp
+  go [] = t
+  go ((nm, pos) :: nms)
+    = IPi fc M0 ImplicitArg (Just nm) (Implicit fc True)
+    $ addConstraint (pos `elem` params.asFunctors)   `{Prelude.Interfaces.Functor}   nm
+    $ addConstraint (pos `elem` params.asBifunctors) `{Prelude.Interfaces.Bifunctor} nm
+    $ go nms
+
+||| Type of proofs that a type satisfies a constraint.
+||| Internally it's vacuous. We don't export the constructor so
+||| that users cannot manufacture buggy proofs.
+export
+data HasImplementation : (intf : a -> Type) -> TTImp -> Type where
+  TrustMeHI : HasImplementation intf t
+
+||| Given
+||| @ intf an interface (e.g. `Functor`, or `Bifunctor`)
+||| @ t    a term corresponding to a (possibly partially applied) type constructor
+||| check whether Idris2 can find a proof that t satisfies the interface.
+export
+hasImplementation : Elaboration m => (intf : a -> Type) -> (t : TTImp) ->
+                    m (Maybe (HasImplementation intf t))
+hasImplementation c t = catch $ do
+  prf <- isType t
+  intf <- quote c
+  ty <- check {expected = Type} $ withParams emptyFC initParameters prf.parameterNames `(~(intf) ~(t))
+  ignore $ check {expected = ty} `(%search)
+  pure TrustMeHI
+
+------------------------------------------------------------------------------
+-- Core machinery: being functorial
+
+||| IsFunctorialIn is parametrised by
+||| @ t  the name of the data type whose constructors are being analysed
+||| @ x  the name of the type variable that the functioral action will change
+||| @ ty the type being analysed
+||| The inductive type delivers a proof that x occurs positively in ty,
+||| assuming that t also is positive.
+public export
+data IsFunctorialIn : (t, x : Name) -> (ty : TTImp) -> Type
+
+||| FreeOf is parametrised by
+||| @ x  the name of the type variable that the functioral action will change
+||| @ ty the type that does not contain any mention of x
+export
+data FreeOf : (x : Name) -> (ty : TTImp) -> Type
+
+data IsFunctorialIn : (t, x : Name) -> TTImp -> Type where
+  ||| The type variable x occurs alone
+  FIVar : IsFunctorialIn t x (IVar fc x)
+  ||| There is a recursive subtree of type (t a1 ... an u) and u is functorial in x.
+  ||| We do not insist that u is exactly x so that we can deal with nested types
+  ||| like the following:
+  |||   data Full a = Leaf a | Node (Full (a, a))
+  |||   data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
+  FIRec : (0 _ : IsAppView (_, t) _ f) -> IsFunctorialIn t x arg -> IsFunctorialIn t x (IApp fc f arg)
+  ||| The subterm is delayed (either Inf or Lazy)
+  FIDelayed : IsFunctorialIn t x ty -> IsFunctorialIn t x (IDelayed fc lr ty)
+  ||| There are nested subtrees somewhere inside a 3rd party type constructor
+  ||| which satisfies the Bifunctor interface
+  FIBifun : HasImplementation Bifunctor sp ->
+            IsFunctorialIn t x arg1 -> Either (IsFunctorialIn t x arg2) (FreeOf x arg2) ->
+            IsFunctorialIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)
+  ||| There are nested subtrees somewhere inside a 3rd party type constructor
+  ||| which satisfies the Functor interface
+  FIFun : HasImplementation Functor sp ->
+          IsFunctorialIn t x arg -> IsFunctorialIn t x (IApp fc sp arg)
+  ||| A pi type, with no negative occurence of x in its domain
+  FIPi : FreeOf x a -> IsFunctorialIn t x b -> IsFunctorialIn t x (IPi fc rig pinfo nm a b)
+  ||| A type free of x is trivially Functorial in it
+  FIFree : FreeOf x a -> IsFunctorialIn t x a
+
+data FreeOf : Name -> TTImp -> Type where
+  ||| For now we do not bother keeping precise track of the proof that a type
+  ||| is free of x
+  TrustMeFO : FreeOf a x
+
+elemPos : Eq a => a -> List a -> Maybe Nat
+elemPos x = go 0 where
+
+  go : Nat -> List a -> Maybe Nat
+  go idx [] = Nothing
+  go idx (y :: ys) = idx <$ guard (x == y) <|> go (S idx) ys
+
+parameters
+  {0 m : Type -> Type}
+  {auto elab : Elaboration m}
+  {auto error : MonadError Error m}
+  {auto cs : MonadState Parameters m}
+  (t : Name)
+  (ps : List Name)
+  (x : Name)
+
+  ||| When analysing the type of a constructor for the type family t,
+  ||| we hope to observe
+  |||   1. either that it is functorial in x
+  |||   2. or that it is free of x
+  ||| If if it is not the case, we will use the `MonadError Error` constraint
+  ||| to fail with an informative message.
+  public export
+  TypeView : TTImp -> Type
+  TypeView ty = Either (IsFunctorialIn t x ty) (FreeOf x ty)
+
+  ||| Hoping to observe that ty is functorial
+  export
+  typeView : (ty : TTImp) -> m (TypeView ty)
+
+  ||| To avoid code duplication in typeView, we have an auxiliary function
+  ||| specifically to handle the application case
+  typeAppView : {fc : FC} -> (f, arg : TTImp) -> m (TypeView (IApp fc f arg))
+
+  typeAppView {fc} f arg = do
+    chka <- typeView arg
+    case chka of
+      -- if x is present in the argument then the function better be:
+      -- 1. either an occurrence of t i.e. a subterm
+      -- 2. or a type constructor already known to be functorial
+      Left sp => do
+        let Just (MkAppView (_, hd) ts prf) = appView f
+           | _ => throwError (NotAnApplication f)
+        case decEq t hd of
+          Yes Refl => pure $ Left (FIRec prf sp)
+          No diff => case !(hasImplementation Functor f) of
+            Just prf => pure (Left (FIFun prf sp))
+            Nothing => case hd `elemPos` ps of
+              Just n => do
+                -- record that the nth parameter should be functorial
+                ns <- gets asFunctors
+                let ns = ifThenElse (n `elem` ns) ns (n :: ns)
+                modify { asFunctors := ns }
+                -- and happily succeed
+                logMsg "derive.functor.assumption" 10 $
+                  "I am assuming that the parameter \{show hd} is a Functor"
+                pure (Left (FIFun TrustMeHI sp))
+              Nothing => throwError (NotAFunctor f)
+      -- Otherwise it better be the case that f is also free of x so that
+      -- we can mark the whole type as being x-free.
+      Right fo => do
+        Right _ <- typeView f
+          | _ => throwError (NotAFunctorInItsLastArg (IApp fc f arg))
+        pure (Right TrustMeFO)
+
+  typeView (IVar fc y) = pure $ case decEq x y of
+    Yes Refl => Left FIVar
+    No _ => Right TrustMeFO
+  typeView ty@(IPi fc rig pinfo nm a b) = do
+    Right p <- typeView a
+      | _ => throwError (NegativeOccurence x ty)
+    Left q <- typeView b
+      | _ => pure (Right TrustMeFO)
+    pure (Left (FIPi p q))
+  typeView fa@(IApp _ (IApp _ f arg1) arg2) = do
+    chka1 <- typeView arg1
+    case chka1 of
+      Right _ => typeAppView (assert_smaller fa (IApp _ f arg1)) arg2
+      Left sp => case !(hasImplementation Bifunctor f) of
+        Just prf => pure (Left (FIBifun prf sp !(typeView arg2)))
+        Nothing => do
+          let Just (MkAppView (_, hd) ts prf) = appView f
+             | _ => throwError (NotAnApplication f)
+          case hd `elemPos` ps of
+            Just n => do
+              -- record that the nth parameter should be bifunctorial
+              ns <- gets asBifunctors
+              let ns = ifThenElse (n `elem` ns) ns (n :: ns)
+              modify { asBifunctors := ns }
+              -- and happily succeed
+              logMsg "derive.functor.assumption" 10 $
+                  "I am assuming that the parameter \{show hd} is a Bifunctor"
+              pure (Left (FIBifun TrustMeHI sp !(typeView arg2)))
+            Nothing => throwError (NotABifunctor f)
+  typeView fa@(IApp _ f arg) = typeAppView f arg
+  typeView (IDelayed _ lz f) = pure $ case !(typeView f) of
+    Left sp => Left (FIDelayed sp)
+    Right _ => Right TrustMeFO
+  typeView (IPrimVal _ _) = pure (Right TrustMeFO)
+  typeView (IType _) = pure (Right TrustMeFO)
+  typeView ty = throwError (UnsupportedType ty)
+
+------------------------------------------------------------------------------
+-- Core machinery: building the mapping function from an IsFunctorialIn proof
+
+||| We often apply multiple arguments, this makes things simpler
+apply : FC -> TTImp -> List TTImp -> TTImp
+apply fc = foldl (IApp fc)
+
+parameters (fc : FC) (mutualWith : List Name)
+
+  ||| functorFun takes
+  ||| @ mutualWith a list of mutually defined type constructors. Calls to their
+  ||| respective mapping functions typically need an assert_total because the
+  ||| termination checker is not doing enough inlining to see that things are
+  ||| terminating
+  ||| @ assert records whether we should mark recursive calls as total because
+  ||| we are currently constructing the argument to a higher order function
+  ||| which will obscure the termination argument. Starts as `Nothing`, becomes
+  ||| `Just False` if an `assert_total` has already been inserted.
+  ||| @ ty the type being transformed by the mapping function
+  ||| @ rec the name of the mapping function being defined (used for recursive calls)
+  ||| @ f the name of the function we're mapping
+  ||| @ arg the (optional) name of the argument being mapped over. This lets us use
+  ||| Nothing when generating arguments to higher order functions so that we generate
+  ||| the eta contracted `map (mapTree f)` instead of `map (\ ts => mapTree f ts)`.
+  functorFun : (assert : Maybe Bool) -> {ty : TTImp} -> IsFunctorialIn t x ty ->
+               (rec, f : Name) -> (arg : Maybe TTImp) -> TTImp
+  functorFun assert FIVar rec f t = apply fc (IVar fc f) (toList t)
+  functorFun assert (FIRec y sp) rec f t
+    -- only add assert_total if it is declared to be needed
+    = ifThenElse (fromMaybe False assert) (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
+    $ apply fc (IVar fc rec) (functorFun (Just False) sp rec f Nothing :: toList t)
+  functorFun assert (FIDelayed sp) rec f Nothing
+    -- here we need to eta-expand to avoid "Lazy t does not unify with t" errors
+    = let nm = UN $ Basic "eta" in
+      ILam fc MW ExplicitArg (Just nm) (Implicit fc False)
+    $ IDelay fc
+    $ functorFun assert sp rec f (Just (IVar fc nm))
+  functorFun assert (FIDelayed sp) rec f (Just t) = functorFun assert sp rec f (Just t)
+  functorFun assert {ty = IApp _ ty _} (FIFun _ sp) rec f t
+    -- only add assert_total if we are calling a mutually defined Functor implementation.
+    = let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
+      ifThenElse isMutual (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
+    $ apply fc (IVar fc (UN $ Basic "map"))
+      (functorFun ((False <$ guard isMutual) <|> assert <|> Just True) sp rec f Nothing
+       :: toList t)
+  functorFun assert (FIBifun _ sp1 (Left sp2)) rec f t
+    = apply fc (IVar fc (UN $ Basic "bimap"))
+      (functorFun (assert <|> Just True) sp1 rec f Nothing
+      :: functorFun (assert <|> Just True) sp2 rec f Nothing
+      :: toList t)
+  functorFun assert (FIBifun _ sp (Right _)) rec f t
+    = apply fc (IVar fc (UN $ Basic "mapFst"))
+      (functorFun (assert <|> Just True) sp rec f Nothing
+      :: toList t)
+  functorFun assert (FIPi {rig, pinfo, nm} _ sp) rec f (Just t)
+    = let nm = fromMaybe (UN $ Basic "x") nm in
+      -- /!\ We cannot use the type stored in FIPi here because it could just
+      -- be a name that will happen to be different when bound on the LHS!
+      -- Cf. the Free test case in reflection017
+      ILam fc rig pinfo (Just nm) (Implicit fc False)
+    $ functorFun assert sp rec f (Just $ IApp fc t (IVar fc nm))
+  functorFun assert (FIPi {rig, pinfo, nm} _ sp) rec f Nothing
+    = let tnm = UN $ Basic "t" in
+      let nm = fromMaybe (UN $ Basic "x") nm in
+      ILam fc MW ExplicitArg (Just tnm) (Implicit fc False) $
+      -- /!\ We cannot use the type stored in FIPi here because it could just
+      -- be a name that will happen to be different when bound on the LHS!
+      -- Cf. the Free test case in reflection017
+      ILam fc rig pinfo (Just nm) (Implicit fc False) $
+      functorFun assert sp rec f (Just $ IApp fc (IVar fc tnm) (IVar fc nm))
+  functorFun assert (FIFree y) rec f t = fromMaybe `(id) t
+
+------------------------------------------------------------------------------
+-- User-facing: Functor deriving
+
+record ConstructorView where
+  constructor MkConstructorView
+  params      : List Name
+  functorPara : Name
+  conArgTypes : List TTImp
+
+explicits : TTImp -> Maybe ConstructorView
+explicits (IPi fc rig ExplicitArg x a b) = { conArgTypes $= (a ::) } <$> explicits b
+explicits (IPi fc rig pinfo x a b) = explicits b
+explicits (IApp _ f (IVar _ a)) = do
+  MkAppView _ ts _ <- appView f
+  let ps = flip mapMaybe ts $ \ t => the (Maybe Name) $ case t of
+             Arg _ (IVar _ nm) => Just nm
+             _ => Nothing
+  pure (MkConstructorView (ps <>> []) a [])
+explicits _ = Nothing
+
+cleanup : TTImp -> TTImp
+cleanup = \case
+  IVar fc n => IVar fc (dropNS n)
+  t => t
+
+namespace Functor
+
+  derive' : (Elaboration m, MonadError Error m) =>
+            {default Private vis : Visibility} ->
+            {default Total treq : TotalReq} ->
+            {default [] mutualWith : List Name} ->
+            m (Functor f)
+  derive' = do
+
+    -- expand the mutualwith names to have the internal, fully qualified, names
+    mutualWith <- map concat $ for mutualWith $ \ nm => do
+                    ntys <- getType nm
+                    pure (fst <$> ntys)
+
+    -- The goal should have the shape (Functor t)
+    Just (IApp _ (IVar _ functor) t) <- goal
+      | _ => throwError InvalidGoal
+    when (`{Prelude.Interfaces.Functor} /= functor) $
+      logMsg "derive.functor" 1 "Expected to derive Functor but got \{show functor}"
+
+    -- t should be a type constructor
+    logMsg "derive.functor" 1 "Deriving Functor for \{showPrec App $ mapTTImp cleanup t}"
+    MkIsType f params cs <- isType t
+    logMsg "derive.functor.constructors" 1 $
+      joinBy "\n" $ "" :: map (\ (n, ty) => "  \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
+
+    -- Generate a clause for each data constructor
+    let fc = emptyFC
+    let un = UN . Basic
+    let mapName = un ("map" ++ show (dropNS f))
+    let funName = un "f"
+    let fun  = IVar fc funName
+    (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
+      withError (WhenCheckingConstructor cName) $ do
+        -- Grab the types of the constructor's explicit arguments
+        let Just (MkConstructorView paras para args) = explicits ty
+              | _ => throwError ConfusingReturnType
+        logMsg "derive.functor.clauses" 10 $
+          "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup) args)})"
+        let vars = map (IVar fc . un . ("x" ++) . show . (`minus` 1))
+                 $ zipWith const [1..length args] args -- fix because [1..0] is [1,0]
+        recs <- for (zip vars args) $ \ (v, arg) => do
+                  res <- withError (WhenCheckingArg (mapTTImp cleanup arg)) $
+                           typeView f paras para arg
+                  pure $ case res of
+                    Left sp => functorFun fc mutualWith Nothing sp mapName funName (Just v)
+                    Right free => v
+        pure $ PatClause fc
+          (apply fc (IVar fc mapName) [ fun, apply fc (IVar fc cName) vars])
+          (apply fc (IVar fc cName) recs)
+
+    -- Generate the type of the mapping function
+    let paramNames = fst <$> params
+    let a = un $ freshName paramNames "a"
+    let b = un $ freshName paramNames "b"
+    let va = IVar fc a
+    let vb = IVar fc b
+    let ty = MkTy fc fc mapName $ withParams fc ns params
+           $ IPi fc M0 ImplicitArg (Just a) (IType fc)
+           $ IPi fc M0 ImplicitArg (Just b) (IType fc)
+           $ `((~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(t) ~(vb))
+    logMsg "derive.functor.clauses" 1 $
+      joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
+                      :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
+
+    -- Define the instance
+    check $ ILocal fc
+      [ IClaim fc MW vis [Totality treq] ty
+      , IDef fc mapName cls
+      ] `(MkFunctor {f = ~(t)} ~(IVar fc mapName))
+
+  ||| Derive an implementation of Functor for a type constructor.
+  ||| This can be used like so:
+  ||| ```
+  ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
+  ||| treeFunctor : Functor Tree
+  ||| treeFunctor = %runElab derive
+  ||| ```
+  export
+  derive : {default Private vis : Visibility} ->
+           {default Total treq : TotalReq} ->
+           {default [] mutualWith : List Name} ->
+           Elab (Functor f)
+  derive = do
+    res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
+    case res of
+      Left err => fail (show err)
+      Right prf => pure prf
diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
index ae482de7e..de51fd975 100644
--- a/libs/base/Language/Reflection.idr
+++ b/libs/base/Language/Reflection.idr
@@ -205,3 +205,14 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   getLocalType        = lift . getLocalType
   getCons             = lift . getCons
   declare             = lift . declare
+
+||| Catch failures and use the `Maybe` monad instead
+export
+catch : Elaboration m => Elab a -> m (Maybe a)
+catch elab = try (Just <$> elab) (pure Nothing)
+
+||| Run proof search to attempt to find a value of the input type.
+||| Useful to check whether a give interface constraint is satisfied.
+export
+search : Elaboration m => (ty : Type) -> m (Maybe ty)
+search ty = catch $ check {expected = ty} `(%search)
diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr
index e4ce80f39..10467b8f4 100644
--- a/libs/base/Language/Reflection/TTImp.idr
+++ b/libs/base/Language/Reflection/TTImp.idr
@@ -462,6 +462,8 @@ Eq TTImp where
 
   _ == _ = False
 
+public export
+data Mode = InDecl | InCase
 
 mutual
 
@@ -507,7 +509,7 @@ mutual
       = unwords [ show vis
                 , showTotalReq treq (show dt)
                 ]
-    show (IDef fc nm xs) = joinBy "; " (map show xs)
+    show (IDef fc nm xs) = joinBy "; " (map (showClause InDecl) xs)
     show (IParameters fc params decls)
       = unwords
       [ "parameters"
@@ -538,16 +540,19 @@ mutual
     show (ISetFieldApp path s) = "\{joinBy "->" path} $= \{show s}"
 
   export
-  Show Clause where
-    show (PatClause fc lhs rhs) = "\{show lhs} => \{show rhs}"
-    show (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
+  showClause : Mode -> Clause -> String
+  showClause mode (PatClause fc lhs rhs) = "\{show lhs} \{showSep mode} \{show rhs}" where
+    showSep : Mode -> String
+    showSep InDecl = "="
+    showSep InCase = "=>"
+  showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
       = unwords
       [ show lhs, "with"
       , showCount rig $ maybe id (\ nm => (++ " proof \{show nm}")) prf
                       $ showParens True (show wval)
-      , "{", joinBy "; " (assert_total $ map show cls), "}"
+      , "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}"
       ]
-    show (ImpossibleClause fc lhs) = "\{show lhs} impossible"
+  showClause mode (ImpossibleClause fc lhs) = "\{show lhs} impossible"
 
   collectPis : Count -> PiInfo TTImp -> SnocList Name -> TTImp -> TTImp -> (List Name, TTImp)
   collectPis rig pinfo xs argTy t@(IPi fc rig' pinfo' x argTy' retTy)
@@ -568,6 +573,8 @@ mutual
     showPrec d (IVar fc nm) = showPrefix True nm
     showPrec d (IPi fc MW ExplicitArg Nothing argTy retTy)
       = showParens (d > Open) $ "\{showPrec Dollar argTy} -> \{show retTy}"
+    showPrec d (IPi fc MW AutoImplicit Nothing argTy retTy)
+      = showParens (d > Open) $ "\{showPrec Dollar argTy} => \{show retTy}"
     showPrec d (IPi fc rig pinfo x argTy retTy)
       = showParens (d > Open) $
           let (xs, retTy) = collectPis rig pinfo [<fromMaybe (UN Underscore) x] argTy retTy in
@@ -582,7 +589,7 @@ mutual
     showPrec d (ICase fc s ty xs)
       = showParens (d > Open) $
           unwords $ [ "case", show s ] ++ typeFor ty ++ [ "of", "{"
-                    , joinBy "; " (assert_total $ map show xs)
+                    , joinBy "; " (assert_total $ map (showClause InCase) xs)
                     , "}"
                     ]
           where
@@ -633,6 +640,40 @@ mutual
       [(_,x)] => "with \{show x} \{show s}"
       _   => "with [\{joinBy ", " $ map (show . snd) ns}] \{show s}"
 
+public export
+data Argument a
+  = Arg FC a
+  | NamedArg FC Name a
+  | AutoArg FC a
+
+public export
+data IsAppView : (FC, Name) -> SnocList (Argument TTImp) -> TTImp -> Type where
+  AVVar : IsAppView (fc, t) [<] (IVar fc t)
+  AVApp : IsAppView x ts f -> IsAppView x (ts :< Arg fc t) (IApp fc f t)
+  AVNamedApp : IsAppView x ts f -> IsAppView x (ts :< NamedArg fc n t) (INamedApp fc f n t)
+  AVAutoApp : IsAppView x ts f -> IsAppView x (ts :< AutoArg fc t) (IAutoApp fc f a)
+
+public export
+record AppView (t : TTImp) where
+  constructor MkAppView
+  head : (FC, Name)
+  args : SnocList (Argument TTImp)
+  0 isAppView : IsAppView head args t
+
+export
+appView : (t : TTImp) -> Maybe (AppView t)
+appView (IVar fc f) = Just (MkAppView (fc, f) [<] AVVar)
+appView (IApp fc f t) = do
+  (MkAppView x ts prf) <- appView f
+  pure (MkAppView x (ts :< Arg fc t) (AVApp prf))
+appView (INamedApp fc f n t) = do
+  (MkAppView x ts prf) <- appView f
+  pure (MkAppView x (ts :< NamedArg fc n t) (AVNamedApp prf))
+appView (IAutoApp fc f t) = do
+  (MkAppView x ts prf) <- appView f
+  pure (MkAppView x (ts :< AutoArg fc t) (AVAutoApp prf))
+appView _ = Nothing
+
 parameters (f : TTImp -> TTImp)
 
   export
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 9cc3ae9c7..d17179cfb 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -85,6 +85,8 @@ modules = Control.App,
 
           Debug.Trace,
 
+          Deriving.Functor,
+
           Decidable.Decidable,
           Decidable.Equality,
           Decidable.Equality.Core,
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index 625804e54..bb19d1dc8 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -104,7 +104,13 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
                                x       => x
              throw $ RunElabFail $ GenericMsg customFC !(reify defs msg')
     elabCon defs "Try" [_, elab1, elab2]
-        = tryUnify (elabScript fc nest env !(evalClosure defs elab1) exp)
+        = tryUnify (do constart <- getNextEntry
+                       res <- elabScript fc nest env !(evalClosure defs elab1) exp
+                       -- We ensure that all of the constraints introduced during the elab script
+                       -- have been solved. This guarantees that we do not mistakenly succeed even
+                       -- though e.g. a proof search got delayed.
+                       solveConstraintsAfter constart inTerm LastChance
+                       pure res)
                    (elabScript fc nest env !(evalClosure defs elab2) exp)
     elabCon defs "LogMsg" [topic, verb, str]
         = do topic' <- evalClosure defs topic
@@ -244,6 +250,7 @@ checkRunElab rig elabinfo nest env fc script exp
          elabtt <- appCon fc defs n [expected]
          (stm, sty) <- runDelays (const True) $
                            check rig elabinfo nest env script (Just (gnf env elabtt))
+         solveConstraints inTerm Normal
          defs <- get Ctxt -- checking might have resolved some holes
          ntm <- elabScript fc nest env
                            !(nfOpts withAll defs env stm) (Just (gnf env expected))
diff --git a/tests/Main.idr b/tests/Main.idr
index 93873b32f..e8b9bed56 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -220,7 +220,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
       ["reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
-       "reflection013", "reflection014", "reflection015", "reflection016"
+       "reflection013", "reflection014", "reflection015", "reflection016",
+       "reflection017"
       ]
 
 idrisTestsWith : TestPool
diff --git a/tests/idris2/reflection017/DeriveFunctor.idr b/tests/idris2/reflection017/DeriveFunctor.idr
new file mode 100644
index 000000000..c6dd8260c
--- /dev/null
+++ b/tests/idris2/reflection017/DeriveFunctor.idr
@@ -0,0 +1,222 @@
+module DeriveFunctor
+
+import Deriving.Functor
+
+%language ElabReflection
+%default covering
+
+%logging "derive.functor.clauses" 1
+%logging "derive.functor.assumption" 10
+
+list : Functor List
+list = %runElab derive
+
+maybe : Functor Maybe
+maybe = %runElab derive
+
+either : Functor (Either err)
+either = %runElab derive
+
+namespace Constant
+
+  record Constant (a, b : Type) where
+    constructor MkConstant
+    runConstant : a
+
+  constant : Functor (Constant a)
+  constant = %runElab derive
+
+namespace Vect
+
+  public export
+  data Vect : Nat -> Type -> Type where
+    Nil : Vect Z a
+    (::) : a -> Vect n a -> Vect (S n) a
+
+  export %hint
+  total
+  vect : Functor (Vect n)
+  vect = %runElab derive
+
+namespace BigTree
+
+  data BigTree a
+    = End a
+    | Branch String (List a) (Bool -> BigTree a)
+    | Rose (List (BigTree a))
+
+  total
+  bigTree : Functor BigTree
+  bigTree = %runElab derive
+
+namespace Matrix
+
+  record Matrix m n a where
+    constructor MkMatrix
+    runMatrix : Vect m (Vect n a)
+
+  total
+  matrix : Functor (Matrix m n)
+  matrix = %runElab derive
+
+namespace Tm
+
+  data Op : Nat -> Type where
+    Neg : Op 1
+    Add : Op 2
+
+  data Tm : Type -> Type where
+    Var : a -> Tm a
+    Call : Op n -> Vect n (Tm a) -> Tm a
+    Lam : Tm (Maybe a) -> Tm a
+
+  total
+  tm : Functor Tm
+  tm = %runElab derive
+
+namespace Forest
+
+  data Tree : Type -> Type
+  data Forest : Type -> Type
+
+  data Tree : Type -> Type where
+    Leaf : a -> Tree a
+    Node : Forest a -> Tree a
+
+  data Forest : Type -> Type where
+    Empty : Forest a
+    Plant : Tree a -> Forest a -> Forest a
+
+  %hint total tree : Functor Tree
+  %hint total forest : Functor Forest
+
+  tree = %runElab derive {mutualWith = [`{Forest}]}
+  forest = %runElab derive {mutualWith = [`{Tree}]}
+
+namespace List1
+
+  data List1 : Type -> Type where
+    MkList1 : (a, Maybe (List1 a)) -> List1 a
+
+  total
+  list1 : Functor List1
+  list1 = %runElab derive
+
+namespace Full
+
+  data Full a = Leaf a | Node (Full (a, a))
+
+  total
+  full : Functor Full
+  full = %runElab derive
+
+failing "Negative occurence of a"
+
+  data NOT : Type -> Type where
+    MkNOT : (a -> Void) -> NOT a
+
+  total
+  negative : Functor NOT
+  negative = %runElab derive
+
+namespace Colist
+
+  data Colist a = Nil | (::) a (Inf (Colist a))
+
+  total
+  colist : Functor Colist
+  colist = %runElab derive
+
+namespace LAZY
+
+  record LAZY (a : Type) where
+    constructor MkLAZY
+    wrapped : Lazy a
+
+  total
+  lazy : Functor LAZY
+  lazy = %runElab derive
+
+namespace Rose
+
+  data Rose a = Node (List (Lazy (Rose a)))
+
+  total
+  rose : Functor Rose
+  rose = %runElab derive
+
+namespace Free
+
+  data Free : (Type -> Type) -> Type -> Type where
+    Pure : a -> Free f a
+    Bind : f a -> (a -> Free f b) -> Free f b
+
+  total
+  free : Functor (Free f)
+  free = %runElab derive
+
+namespace MaybeT
+
+  record MaybeT (m : Type -> Type) (a : Type) where
+    constructor MkMaybeT
+    runMaybeT : m (Maybe a)
+
+  total
+  maybeT : Functor m => Functor (MaybeT m)
+  maybeT = %runElab derive
+
+namespace TreeT
+
+  data TreeT : (Type -> Type -> Type) -> Type -> Type where
+    MkTreeT : layer a (TreeT layer a) -> TreeT layer a
+
+  %hint
+  treeT : Bifunctor layer => Functor (TreeT layer)
+  treeT = %runElab derive {treq = CoveringOnly}
+
+  record Tree (a : Type) where
+    constructor MkTree
+    runTree : TreeT Either a
+
+  tree : Functor Tree
+  tree = %runElab derive {treq = CoveringOnly}
+
+failing "Couldn't find a `Functor' instance for the type constructor DeriveFunctor.Wrap"
+
+  record Wrap (a : Type) where
+    constructor MkWrap
+    unWrap : a
+
+  data Indirect : Type -> Type where
+    MkIndirect : Wrap a -> Indirect a
+
+  total
+  indirect : Functor Indirect
+  indirect = %runElab derive
+
+namespace BifunctorFail
+
+  data Tree : (l, n : Type) -> Type where
+    Leaf : l -> Tree l n
+    Node : Tree l n -> n -> Tree l n -> Tree l n
+
+  -- this one will succeed
+  total
+  tree : Functor (Tree l)
+  tree = %runElab derive
+
+  failing "Couldn't find a `Bifunctor' instance for the type constructor DeriveFunctor.BifunctorFail.Tree"
+
+    record Tree' (a : Type) where
+      constructor MkTree'
+      getTree : Tree a a
+
+    -- and this one will fail
+    tree' : Functor Tree'
+    tree' = %runElab derive
+
+failing "Expected a type constructor, got: Prelude.Basics.id {a = Type}"
+
+  total
+  functor : Functor Prelude.id
+  functor = %runElab derive
diff --git a/tests/idris2/reflection017/Search.idr b/tests/idris2/reflection017/Search.idr
new file mode 100644
index 000000000..ec41c7f24
--- /dev/null
+++ b/tests/idris2/reflection017/Search.idr
@@ -0,0 +1,12 @@
+module Search
+
+import Language.Reflection
+import Language.Reflection.TTImp
+
+%language ElabReflection
+
+nothing : Maybe (Not Nat)
+nothing = %runElab (search ?)
+
+test : Search.nothing === Nothing
+test = Refl
diff --git a/tests/idris2/reflection017/expected b/tests/idris2/reflection017/expected
new file mode 100644
index 000000000..8ce276d01
--- /dev/null
+++ b/tests/idris2/reflection017/expected
@@ -0,0 +1,78 @@
+1/1: Building DeriveFunctor (DeriveFunctor.idr)
+LOG derive.functor.clauses:1: 
+  mapList : {0 a, b : Type} -> (a -> b) -> List a -> List b
+  mapList f Nil = Nil
+  mapList f (x0 :: x1) = (f x0) :: (mapList f x1)
+LOG derive.functor.clauses:1: 
+  mapMaybe : {0 a, b : Type} -> (a -> b) -> Maybe a -> Maybe b
+  mapMaybe f Nothing = Nothing
+  mapMaybe f (Just x0) = Just (f x0)
+LOG derive.functor.clauses:1: 
+  mapEither : {0 err : _} -> {0 a, b : Type} -> (a -> b) -> Either err a -> Either err b
+  mapEither f (Left x0) = Left x0
+  mapEither f (Right x0) = Right (f x0)
+LOG derive.functor.clauses:1: 
+  mapConstant : {0 a : _} -> {0 a0, b : Type} -> (a0 -> b) -> Constant a a0 -> Constant a b
+  mapConstant f (MkConstant x0) = MkConstant x0
+LOG derive.functor.clauses:1: 
+  mapVect : {0 n : _} -> {0 a, b : Type} -> (a -> b) -> Vect n a -> Vect n b
+  mapVect f Nil = Nil
+  mapVect f (x0 :: x1) = (f x0) :: (mapVect f x1)
+LOG derive.functor.clauses:1: 
+  mapBigTree : {0 a, b : Type} -> (a -> b) -> BigTree a -> BigTree b
+  mapBigTree f (End x0) = End (f x0)
+  mapBigTree f (Branch x0 x1 x2) = Branch x0 (map f x1) (\ {arg:4047} => mapBigTree f (x2 {arg:4047}))
+  mapBigTree f (Rose x0) = Rose (map (assert_total (mapBigTree f)) x0)
+LOG derive.functor.clauses:1: 
+  mapMatrix : {0 n, m : _} -> {0 a, b : Type} -> (a -> b) -> Matrix m n a -> Matrix m n b
+  mapMatrix f (MkMatrix x0) = MkMatrix (map (map f) x0)
+LOG derive.functor.clauses:1: 
+  mapTm : {0 a, b : Type} -> (a -> b) -> Tm a -> Tm b
+  mapTm f (Var x0) = Var (f x0)
+  mapTm f (Call x0 x1) = Call x0 (map (assert_total (mapTm f)) x1)
+  mapTm f (Lam x0) = Lam (mapTm (map f) x0)
+LOG derive.functor.clauses:1: 
+  mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
+  mapTree f (Leaf x0) = Leaf (f x0)
+  mapTree f (Node x0) = Node (assert_total (map f x0))
+LOG derive.functor.clauses:1: 
+  mapForest : {0 a, b : Type} -> (a -> b) -> Forest a -> Forest b
+  mapForest f Empty = Empty
+  mapForest f (Plant x0 x1) = Plant (assert_total (map f x0)) (mapForest f x1)
+LOG derive.functor.clauses:1: 
+  mapList1 : {0 a, b : Type} -> (a -> b) -> List1 a -> List1 b
+  mapList1 f (MkList1 x0) = MkList1 (bimap f (map (assert_total (mapList1 f))) x0)
+LOG derive.functor.clauses:1: 
+  mapFull : {0 a, b : Type} -> (a -> b) -> Full a -> Full b
+  mapFull f (Leaf x0) = Leaf (f x0)
+  mapFull f (Node x0) = Node (mapFull (bimap f f) x0)
+LOG derive.functor.clauses:1: 
+  mapColist : {0 a, b : Type} -> (a -> b) -> Colist a -> Colist b
+  mapColist f Nil = Nil
+  mapColist f (x0 :: x1) = (f x0) :: (mapColist f x1)
+LOG derive.functor.clauses:1: 
+  mapLAZY : {0 a, b : Type} -> (a -> b) -> LAZY a -> LAZY b
+  mapLAZY f (MkLAZY x0) = MkLAZY (f x0)
+LOG derive.functor.clauses:1: 
+  mapRose : {0 a, b : Type} -> (a -> b) -> Rose a -> Rose b
+  mapRose f (Node x0) = Node (map (\ eta => Delay (assert_total (mapRose f eta))) x0)
+LOG derive.functor.clauses:1: 
+  mapFree : {0 f : _} -> {0 a, b : Type} -> (a -> b) -> Free f a -> Free f b
+  mapFree f (Pure x0) = Pure (f x0)
+  mapFree f (Bind x0 x1) = Bind x0 (\ {arg:5076} => mapFree f (x1 {arg:5076}))
+LOG derive.functor.assumption:10: I am assuming that the parameter m is a Functor
+LOG derive.functor.clauses:1: 
+  mapMaybeT : {0 m : _} -> Functor m => {0 a, b : Type} -> (a -> b) -> MaybeT m a -> MaybeT m b
+  mapMaybeT f (MkMaybeT x0) = MkMaybeT (map (map f) x0)
+LOG derive.functor.assumption:10: I am assuming that the parameter layer is a Bifunctor
+LOG derive.functor.clauses:1: 
+  mapTreeT : {0 layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT layer a -> TreeT layer b
+  mapTreeT f (MkTreeT x0) = MkTreeT (bimap f (assert_total (mapTreeT f)) x0)
+LOG derive.functor.clauses:1: 
+  mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
+  mapTree f (MkTree x0) = MkTree (map f x0)
+LOG derive.functor.clauses:1: 
+  mapTree : {0 l : _} -> {0 a, b : Type} -> (a -> b) -> Tree l a -> Tree l b
+  mapTree f (Leaf x0) = Leaf x0
+  mapTree f (Node x0 x1 x2) = Node (mapTree f x0) (f x1) (mapTree f x2)
+1/1: Building Search (Search.idr)
diff --git a/tests/idris2/reflection017/run b/tests/idris2/reflection017/run
new file mode 100755
index 000000000..f749b8343
--- /dev/null
+++ b/tests/idris2/reflection017/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner -c DeriveFunctor.idr
+$1 --no-color --console-width 0 --no-banner -c Search.idr