Wingman doesn't respect fundeps

[isovector]

Preamble:

class Monoid doc => HasObject doc ndoc | doc -> ndoc, ndoc -> doc where
instance HasObject SwaggerDoc NamedSwaggerDoc where

object ::
  HasObject doc doc' =>
  Text ->
  SchemaP doc A.Object [A.Pair] a b ->
  SchemaP doc' A.Value A.Value a b

class ToSchema a where
  schema :: ValueSchema NamedSwaggerDoc A.Value A.Value a a

if we check in the context of this:

instance ToSchema Rec where
  schema = [wingman| use object
                   , use undefined
                   |]

we get a hole ⊢ SchemaP doc Object [Pair] Rec Rec

but this should actually be SchemaP SwaggerDoc Object [Pair] Rec Rec as per the fundep.

[isovector]

Pretty easy fix, all things considered:

apply :: Saturation -> HyInfo CType -> TacticsM ()
apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do
  jdg <- goal
  let g  = jGoal jdg
      ty = unCType $ hi_type hi
      func = hi_name hi
  ty' <- freshTyvars ty
  let (_, theta, all_args, ret) = tacticsSplitFunTy ty'
      saturated_args = dropEnd n all_args
      unsaturated_args = takeEnd n all_args
  ctx <- ask
  skolems <- gets ts_skolems
  rule $ \jdg -> do
    unify g (CType $ mkVisFunTys unsaturated_args ret)
    subst <- gets ts_unifier
    let theta' = substTheta subst theta
    let fundeps = foldMap (foldMap fd_eqs . improveFromInstEnv (ctxInstEnvs ctx) (\_ _ -> ())) theta'
        unified = tryUnifyUnivarsButNotSkolemsMany skolems fundeps
    modify $ updateSubst $ maybe emptyTCvSubst id unified

    ext
        <- fmap unzipTrace
        $ traverse ( newSubgoal
                    . blacklistingDestruct
                    . flip withNewGoal jdg
                    . CType
                    . scaledThing
                    ) saturated_args
    pure $
      ext
        & #syn_used_vals %~ (\x -> S.insert func x <> getAncestry jdg func)
        & #syn_val       %~ mkApply func . fmap unLoc