    {-|
    Copyright  :  (C) 2016     , University of Twente,
                      2017-2018, QBayLogic B.V.,
                      2017     , Google Inc.
    License    :  BSD2 (see the file LICENSE)
    Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

    A type checker plugin for GHC that can derive \"complex\" @KnownNat@
    constraints from other simple/variable @KnownNat@ constraints. i.e. without
    this plugin, you must have both a @KnownNat n@ and a @KnownNat (n+2)@
    constraint in the type signature of the following function:

    @
    f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
    @

    Using the plugin you can omit the @KnownNat (n+2)@ constraint:

    @
    f :: forall n . KnownNat n => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
    @

    The plugin can derive @KnownNat@ constraints for types consisting of:

    * Type variables, when there is a corresponding @KnownNat@ constraint
    * Type-level naturals
    * Applications of the arithmetic expression: @{+,-,*,^}@
    * Type functions, when there is either:
      * a matching given @KnownNat@ constraint; or
      * a corresponding @KnownNat\<N\>@ instance for the type function

    To elaborate the latter points, given the type family @Min@:

    @
    type family Min (a :: Nat) (b :: Nat) :: Nat where
      Min 0 b = 0
      Min a b = If (a <=? b) a b
    @

    the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a
    @KnownNat (Min x y)@ constraint:

    @
    g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer
    g _ _ = natVal (Proxy :: Proxy (Min x y + 1))
    @

    And, given the type family @Max@:

    @
    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a
    @

    and corresponding @KnownNat2@ instance:

    @
    instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where
      natSing2 = let x = natVal (Proxy @a)
                     y = natVal (Proxy @b)
                     z = max x y
                 in  SNatKn z
      \{\-# INLINE natSing2 \#-\}
    @

    the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a
    @KnownNat x@ and @KnownNat y@ constraint:

    @
    h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
    h _ _ = natVal (Proxy :: Proxy (Max x y + 1))
    @

    To use the plugin, add the

    @
    OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
    @

    Pragma to the header of your file.

    -}

    {-# LANGUAGE CPP           #-}
    {-# LANGUAGE LambdaCase    #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE ViewPatterns  #-}
    {-# LANGUAGE TemplateHaskellQuotes #-}
    {-# LANGUAGE Trustworthy   #-}

    {-# OPTIONS_HADDOCK show-extensions #-}

    module GHC.TypeLits.KnownNat.Solver
      ( plugin )
    where

    -- external

    import Control.Arrow ((&&&), first)
    import Control.Monad.Trans.Maybe (MaybeT (..))
    import Control.Monad.Trans.Writer.Strict
    import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
    import Data.Type.Ord (OrdCond)
    import Data.Type.Bool (If)
    import GHC.TcPluginM.Extra (newWanted, tracePlugin)
    import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..))
    import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)

    -- GHC API

    import GHC.Builtin.Names (knownNatClassName)
    import GHC.Builtin.Types (boolTy)
    import GHC.Builtin.Types.Literals (typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon)
    import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon)
    import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
    import GHC.Core.Class (Class, classMethods, className, classTyCon)
    import GHC.Core.Coercion
      (Coercion, Role (Nominal, Representational), coercionRKind, mkNomReflCo,
       mkTyConAppCo, mkUnivCo)
    import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv)
    import GHC.Core.Make (mkNaturalExpr)
    import GHC.Core.Predicate
      (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType)
    import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv))
    import GHC.Core.TyCon (tyConName)
    #if MIN_VERSION_ghc(9,6,0)
    import GHC.Core.Type
      (PredType, dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,
       piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,
       irrelevantMult)
    import GHC.Core.TyCo.Compare
      (eqType)
    #else
    import GHC.Core.Type
      (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,
       piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind,
       irrelevantMult)
    #endif
    import GHC.Data.FastString (fsLit)
    import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
    import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)
    import GHC.Tc.Plugin (TcPluginM, tcLookupClass, getInstEnvs, unsafeTcPluginTcM, tcPluginIO, tcLookupTyCon)
    import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform, env_top)
    import GHC.Tc.Types.Constraint
      (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical)
    #if MIN_VERSION_ghc(9,6,0)
    import GHC.Tc.Types.Evidence
      (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, evTermCoercion_maybe)
    import GHC.Plugins
      (mkSymCo, mkTransCo)
    #else
    import GHC.Tc.Types.Evidence
      (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo,
       evTermCoercion_maybe)
    #endif
    import GHC.Types.Id (idType)
    import GHC.Types.Name (nameModule_maybe, nameOccName, Name)
    import GHC.Types.Name.Occurrence (occNameString)
    import GHC.Types.Unique.FM (emptyUFM)
    import GHC.Types.Var (DFunId)
    import GHC.Unit.Module (moduleName, moduleNameString)
    import qualified Language.Haskell.TH as TH
    import GHC.Plugins (thNameToGhcNameIO, TyCon)
    import GHC.Driver.Env (hsc_NC)
    import GHC.Data.IOEnv (getEnv)
    import GHC.TypeLits.KnownNat

    #if MIN_VERSION_ghc(9,6,0)
    mkTcSymCo :: Coercion -> Coercion
    mkTcSymCo :: Coercion -> Coercion
    mkTcSymCo = Coercion -> Coercion
    mkSymCo

    mkTcTransCo :: Coercion -> Coercion -> Coercion
    mkTcTransCo :: Coercion -> Coercion -> Coercion
    mkTcTransCo = Coercion -> Coercion -> Coercion
    mkTransCo
    #endif

    -- | Classes and instances from "GHC.TypeLits.KnownNat"

    data KnownNatDefs
      = KnownNatDefs
      { KnownNatDefs -> Class
    knownBool     :: Class
      , KnownNatDefs -> Class
    knownBoolNat2 :: Class
      , KnownNatDefs -> Class
    knownNat2Bool :: Class
      , KnownNatDefs -> Int -> Maybe Class
    knownNatN     :: Int -> Maybe Class -- ^ KnownNat{N}

      , KnownNatDefs -> TyCon
    ordCondTyCon  :: TyCon
      , KnownNatDefs -> TyCon
    ifTyCon       :: TyCon
      }

    -- | Simple newtype wrapper to distinguish the original (flattened) argument of

    -- knownnat from the un-flattened version that we work with internally.

    newtype Orig a = Orig { forall a. Orig a -> a
    unOrig :: a }

    -- | KnownNat constraints

    type KnConstraint = (Ct    -- The constraint

                        ,Class -- KnownNat class

                        ,Type  -- The argument to KnownNat

                        ,Orig Type  -- Original, flattened, argument to KnownNat

                        )

    {-|
    A type checker plugin for GHC that can derive \"complex\" @KnownNat@
    constraints from other simple/variable @KnownNat@ constraints. i.e. without
    this plugin, you must have both a @KnownNat n@ and a @KnownNat (n+2)@
    constraint in the type signature of the following function:

    @
    f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
    @

    Using the plugin you can omit the @KnownNat (n+2)@ constraint:

    @
    f :: forall n . KnownNat n => Proxy n -> Integer
    f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
    @

    The plugin can derive @KnownNat@ constraints for types consisting of:

    * Type variables, when there is a corresponding @KnownNat@ constraint
    * Type-level naturals
    * Applications of the arithmetic expression: @{+,-,*,^}@
    * Type functions, when there is either:
      * a matching given @KnownNat@ constraint; or
      * a corresponding @KnownNat\<N\>@ instance for the type function

    To elaborate the latter points, given the type family @Min@:

    @
    type family Min (a :: Nat) (b :: Nat) :: Nat where
      Min 0 b = 0
      Min a b = If (a <=? b) a b
    @

    the plugin can derive a @KnownNat (Min x y + 1)@ constraint given only a
    @KnownNat (Min x y)@ constraint:

    @
    g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer
    g _ _ = natVal (Proxy :: Proxy (Min x y + 1))
    @

    And, given the type family @Max@:

    @
    type family Max (a :: Nat) (b :: Nat) :: Nat where
      Max 0 b = b
      Max a b = If (a <=? b) b a

    $(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol
    @

    and corresponding @KnownNat2@ instance:

    @
    instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where
      type KnownNatF2 \"TestFunctions.Max\" = MaxSym0
      natSing2 = let x = natVal (Proxy @ a)
                     y = natVal (Proxy @ b)
                     z = max x y
                 in  SNatKn z
      \{\-# INLINE natSing2 \#-\}
    @

    the plugin can derive a @KnownNat (Max x y + 1)@ constraint given only a
    @KnownNat x@ and @KnownNat y@ constraint:

    @
    h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
    h _ _ = natVal (Proxy :: Proxy (Max x y + 1))
    @

    To use the plugin, add the

    @
    OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
    @

    Pragma to the header of your file.

    -}
    plugin :: Plugin
    plugin :: Plugin
    plugin
      = Plugin
    defaultPlugin
      { tcPlugin = const $ Just normalisePlugin
    #if MIN_VERSION_ghc(8,6,0)
      , pluginRecompile = purePlugin
    #endif
      }

    normalisePlugin :: TcPlugin
    normalisePlugin :: TcPlugin
    normalisePlugin = CommandLineOption -> TcPlugin -> TcPlugin
    tracePlugin CommandLineOption
    "ghc-typelits-knownnat"
      TcPlugin { tcPluginInit :: TcPluginM KnownNatDefs
    tcPluginInit  = TcPluginM KnownNatDefs
    lookupKnownNatDefs
               , tcPluginSolve :: KnownNatDefs -> TcPluginSolver
    tcPluginSolve = KnownNatDefs -> TcPluginSolver
    solveKnownNat
               , tcPluginRewrite :: KnownNatDefs -> UniqFM TyCon TcPluginRewriter
    tcPluginRewrite = UniqFM TyCon TcPluginRewriter
    -> KnownNatDefs -> UniqFM TyCon TcPluginRewriter
    forall a b. a -> b -> a
    const UniqFM TyCon TcPluginRewriter
    forall key elt. UniqFM key elt
    emptyUFM
               , tcPluginStop :: KnownNatDefs -> TcPluginM ()
    tcPluginStop  = TcPluginM () -> KnownNatDefs -> TcPluginM ()
    forall a b. a -> b -> a
    const (() -> TcPluginM ()
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
               }

    solveKnownNat :: KnownNatDefs -> EvBindsVar -> [Ct] -> [Ct]
                  -> TcPluginM TcPluginSolveResult
    solveKnownNat :: KnownNatDefs -> TcPluginSolver
    solveKnownNat KnownNatDefs
    _defs EvBindsVar
    _ [Ct]
    _givens []      = TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk [] [])
    solveKnownNat KnownNatDefs
    defs  EvBindsVar
    _ [Ct]
    givens  [Ct]
    wanteds = do
      let kn_wanteds :: [(Ct, Class, Type, Orig Type)]
    kn_wanteds = ((Ct, Class, Type, Orig Type) -> (Ct, Class, Type, Orig Type))
    -> [(Ct, Class, Type, Orig Type)] -> [(Ct, Class, Type, Orig Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Ct
    x,Class
    y,Type
    z,Orig Type
    orig) -> (Ct
    x,Class
    y,Type
    z,Orig Type
    orig))
                     ([(Ct, Class, Type, Orig Type)] -> [(Ct, Class, Type, Orig Type)])
    -> [(Ct, Class, Type, Orig Type)] -> [(Ct, Class, Type, Orig Type)]
    forall a b. (a -> b) -> a -> b
    $ (Ct -> Maybe (Ct, Class, Type, Orig Type))
    -> [Ct] -> [(Ct, Class, Type, Orig Type)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (KnownNatDefs -> Ct -> Maybe (Ct, Class, Type, Orig Type)
    toKnConstraint KnownNatDefs
    defs) [Ct]
    wanteds
      case [(Ct, Class, Type, Orig Type)]
    kn_wanteds of
        [] -> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk [] [])
        [(Ct, Class, Type, Orig Type)]
    _  -> do
          -- Make a lookup table for all the [G]iven constraints

          let given_map :: [(CType, EvExpr)]
    given_map = (Ct -> (CType, EvExpr)) -> [Ct] -> [(CType, EvExpr)]
    forall a b. (a -> b) -> [a] -> [b]
    map Ct -> (CType, EvExpr)
    toGivenEntry [Ct]
    givens

          -- Try to solve the wanted KnownNat constraints given the [G]iven

          -- KnownNat constraints

          ([(EvTerm, Ct)]
    solved,[[Ct]]
    new) <- ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]]))
    -> ([Maybe ((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])])
    -> [Maybe ((EvTerm, Ct), [Ct])]
    -> ([(EvTerm, Ct)], [[Ct]])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe ((EvTerm, Ct), [Ct])] -> [((EvTerm, Ct), [Ct])]
    forall a. [Maybe a] -> [a]
    catMaybes) ([Maybe ((EvTerm, Ct), [Ct])] -> ([(EvTerm, Ct)], [[Ct]]))
    -> TcPluginM [Maybe ((EvTerm, Ct), [Ct])]
    -> TcPluginM ([(EvTerm, Ct)], [[Ct]])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (((Ct, Class, Type, Orig Type)
     -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])))
    -> [(Ct, Class, Type, Orig Type)]
    -> TcPluginM [Maybe ((EvTerm, Ct), [Ct])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (KnownNatDefs
    -> [(CType, EvExpr)]
    -> (Ct, Class, Type, Orig Type)
    -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
    constraintToEvTerm KnownNatDefs
    defs [(CType, EvExpr)]
    given_map) [(Ct, Class, Type, Orig Type)]
    kn_wanteds)
          TcPluginSolveResult -> TcPluginM TcPluginSolveResult
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
    TcPluginOk [(EvTerm, Ct)]
    solved ([[Ct]] -> [Ct]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Ct]]
    new))

    -- | Get the KnownNat constraints

    toKnConstraint :: KnownNatDefs -> Ct -> Maybe KnConstraint
    toKnConstraint :: KnownNatDefs -> Ct -> Maybe (Ct, Class, Type, Orig Type)
    toKnConstraint KnownNatDefs
    defs Ct
    ct = case Type -> Pred
    classifyPredType (Type -> Pred) -> Type -> Pred
    forall a b. (a -> b) -> a -> b
    $ CtEvidence -> Type
    ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
    forall a b. (a -> b) -> a -> b
    $ Ct -> CtEvidence
    ctEvidence Ct
    ct of
      ClassPred Class
    cls [Type
    ty]
        |  Class -> Name
    className Class
    cls Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    knownNatClassName Bool -> Bool -> Bool
    ||
           Class -> Name
    className Class
    cls Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Class -> Name
    className (KnownNatDefs -> Class
    knownBool KnownNatDefs
    defs)
        -> (Ct, Class, Type, Orig Type) -> Maybe (Ct, Class, Type, Orig Type)
    forall a. a -> Maybe a
    Just (Ct
    ct,Class
    cls,Type
    ty,Type -> Orig Type
    forall a. a -> Orig a
    Orig Type
    ty)
      Pred
    _ -> Maybe (Ct, Class, Type, Orig Type)
    forall a. Maybe a
    Nothing

    -- | Create a look-up entry for a [G]iven constraint.

    toGivenEntry :: Ct -> (CType,EvExpr)
    toGivenEntry :: Ct -> (CType, EvExpr)
    toGivenEntry Ct
    ct = let ct_ev :: CtEvidence
    ct_ev = Ct -> CtEvidence
    ctEvidence Ct
    ct
                          c_ty :: Type
    c_ty  = CtEvidence -> Type
    ctEvPred   CtEvidence
    ct_ev
                          ev :: EvExpr
    ev    = (() :: Constraint) => CtEvidence -> EvExpr
    CtEvidence -> EvExpr
    ctEvExpr   CtEvidence
    ct_ev
                      in  (Type -> CType
    CType Type
    c_ty,EvExpr
    ev)

    -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat"

    lookupKnownNatDefs :: TcPluginM KnownNatDefs
    lookupKnownNatDefs :: TcPluginM KnownNatDefs
    lookupKnownNatDefs = do
        Class
    kbC    <- Name -> TcPluginM Class
    look ''KnownBool
        Class
    kbn2C  <- Name -> TcPluginM Class
    look ''KnownBoolNat2
        Class
    kn2bC  <- Name -> TcPluginM Class
    look ''KnownNat2Bool
        Class
    kn1C   <- Name -> TcPluginM Class
    look ''KnownNat1
        Class
    kn2C   <- Name -> TcPluginM Class
    look ''KnownNat2
        Class
    kn3C   <- Name -> TcPluginM Class
    look ''KnownNat3
        TyCon
    ordcond <- Name -> TcPluginM Name
    lookupTHName ''OrdCond TcPluginM Name -> (Name -> TcPluginM TyCon) -> TcPluginM TyCon
    forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Name -> TcPluginM TyCon
    tcLookupTyCon
        TyCon
    ifTc <- Name -> TcPluginM Name
    lookupTHName ''If TcPluginM Name -> (Name -> TcPluginM TyCon) -> TcPluginM TyCon
    forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Name -> TcPluginM TyCon
    tcLookupTyCon
        KnownNatDefs -> TcPluginM KnownNatDefs
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return KnownNatDefs
               { knownBool :: Class
    knownBool     = Class
    kbC
               , knownBoolNat2 :: Class
    knownBoolNat2 = Class
    kbn2C
               , knownNat2Bool :: Class
    knownNat2Bool = Class
    kn2bC
               , knownNatN :: Int -> Maybe Class
    knownNatN     = \case { Int
    1 -> Class -> Maybe Class
    forall a. a -> Maybe a
    Just Class
    kn1C
                                       ; Int
    2 -> Class -> Maybe Class
    forall a. a -> Maybe a
    Just Class
    kn2C
                                       ; Int
    3 -> Class -> Maybe Class
    forall a. a -> Maybe a
    Just Class
    kn3C
                                       ; Int
    _ -> Maybe Class
    forall a. Maybe a
    Nothing
                                       }
               , ordCondTyCon :: TyCon
    ordCondTyCon  = TyCon
    ordcond
               , ifTyCon :: TyCon
    ifTyCon       = TyCon
    ifTc
               }
      where
        look :: Name -> TcPluginM Class
    look Name
    nm = Name -> TcPluginM Name
    lookupTHName Name
    nm TcPluginM Name -> (Name -> TcPluginM Class) -> TcPluginM Class
    forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Name -> TcPluginM Class
    tcLookupClass

    lookupTHName :: TH.Name -> TcPluginM Name
    lookupTHName :: Name -> TcPluginM Name
    lookupTHName Name
    th = do
        NameCache
    nc <- TcM NameCache -> TcPluginM NameCache
    forall a. TcM a -> TcPluginM a
    unsafeTcPluginTcM (HscEnv -> NameCache
    hsc_NC (HscEnv -> NameCache)
    -> (Env TcGblEnv TcLclEnv -> HscEnv)
    -> Env TcGblEnv TcLclEnv
    -> NameCache
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Env TcGblEnv TcLclEnv -> HscEnv
    forall gbl lcl. Env gbl lcl -> HscEnv
    env_top (Env TcGblEnv TcLclEnv -> NameCache)
    -> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
    -> TcM NameCache
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
    forall env. IOEnv env env
    getEnv)
        Maybe Name
    res <- IO (Maybe Name) -> TcPluginM (Maybe Name)
    forall a. IO a -> TcPluginM a
    tcPluginIO (IO (Maybe Name) -> TcPluginM (Maybe Name))
    -> IO (Maybe Name) -> TcPluginM (Maybe Name)
    forall a b. (a -> b) -> a -> b
    $ NameCache -> Name -> IO (Maybe Name)
    thNameToGhcNameIO NameCache
    nc Name
    th
        TcPluginM Name
    -> (Name -> TcPluginM Name) -> Maybe Name -> TcPluginM Name
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (CommandLineOption -> TcPluginM Name
    forall a. CommandLineOption -> TcPluginM a
    forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
    fail (CommandLineOption -> TcPluginM Name)
    -> CommandLineOption -> TcPluginM Name
    forall a b. (a -> b) -> a -> b
    $ CommandLineOption
    "Failed to lookup " CommandLineOption -> CommandLineOption -> CommandLineOption
    forall a. [a] -> [a] -> [a]
    ++ Name -> CommandLineOption
    forall a. Show a => a -> CommandLineOption
    show Name
    th) Name -> TcPluginM Name
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Name
    res

    -- | Try to create evidence for a wanted constraint

    constraintToEvTerm
      :: KnownNatDefs
      -- ^ The "magic" KnownNatN classes

      -> [(CType,EvExpr)]
      -- ^ All the [G]iven constraints

      -> KnConstraint
      -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))
    constraintToEvTerm :: KnownNatDefs
    -> [(CType, EvExpr)]
    -> (Ct, Class, Type, Orig Type)
    -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
    constraintToEvTerm KnownNatDefs
    defs [(CType, EvExpr)]
    givens (Ct
    ct,Class
    cls,Type
    op,Orig Type
    orig) = do
        -- 1. Determine if we are an offset apart from a [G]iven constraint

        Maybe (EvTerm, [Ct])
    offsetM <- Type -> TcPluginM (Maybe (EvTerm, [Ct]))
    offset Type
    op
        Maybe (EvTerm, [Ct])
    evM     <- case Maybe (EvTerm, [Ct])
    offsetM of
                     -- 3.a If so, we are done

                     found :: Maybe (EvTerm, [Ct])
    found@Just {} -> Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (EvTerm, [Ct])
    found
                     -- 3.b If not, we check if the outer type-level operation

                     -- has a corresponding KnownNat<N> instance.

                     Maybe (EvTerm, [Ct])
    _ -> (Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm, [Ct]))
    go (Type
    op,Maybe Coercion
    forall a. Maybe a
    Nothing)
        Maybe ((EvTerm, Ct), [Ct])
    -> TcPluginM (Maybe ((EvTerm, Ct), [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((EvTerm -> (EvTerm, Ct)) -> (EvTerm, [Ct]) -> ((EvTerm, Ct), [Ct])
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (,Ct
    ct)) ((EvTerm, [Ct]) -> ((EvTerm, Ct), [Ct]))
    -> Maybe (EvTerm, [Ct]) -> Maybe ((EvTerm, Ct), [Ct])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (EvTerm, [Ct])
    evM)
      where
        -- Determine whether the outer type-level operation has a corresponding

        -- KnownNat<N> instance, where /N/ corresponds to the arity of the

        -- type-level operation

        go :: (Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm,[Ct]))
        go :: (Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm, [Ct]))
    go (Type -> Maybe EvTerm
    go_other -> Just EvTerm
    ev, Maybe Coercion
    _) = Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((EvTerm, [Ct]) -> Maybe (EvTerm, [Ct])
    forall a. a -> Maybe a
    Just (EvTerm
    ev,[]))
        go (ty :: Type
    ty@(TyConApp TyCon
    tc [Type]
    args0), Maybe Coercion
    sM)
          | let tcNm :: Name
    tcNm = TyCon -> Name
    tyConName TyCon
    tc
          , Just Module
    m <- Name -> Maybe Module
    nameModule_maybe Name
    tcNm
          = do
            InstEnvs
    ienv <- TcPluginM InstEnvs
    getInstEnvs
            let mS :: CommandLineOption
    mS  = ModuleName -> CommandLineOption
    moduleNameString (Module -> ModuleName
    forall unit. GenModule unit -> ModuleName
    moduleName Module
    m)
                tcS :: CommandLineOption
    tcS = OccName -> CommandLineOption
    occNameString (Name -> OccName
    nameOccName Name
    tcNm)
                fn0 :: CommandLineOption
    fn0 = CommandLineOption
    mS CommandLineOption -> CommandLineOption -> CommandLineOption
    forall a. [a] -> [a] -> [a]
    ++ CommandLineOption
    "." CommandLineOption -> CommandLineOption -> CommandLineOption
    forall a. [a] -> [a] -> [a]
    ++ CommandLineOption
    tcS
                fn1 :: Type
    fn1 = FastString -> Type
    mkStrLitTy (CommandLineOption -> FastString
    fsLit CommandLineOption
    fn0)
                args1 :: [Type]
    args1 = Type
    fn1Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args0
                instM :: Maybe (ClsInst, Class, [Type], [Type])
    instM = case () of
                  () | Just Class
    knN_cls    <- KnownNatDefs -> Int -> Maybe Class
    knownNatN KnownNatDefs
    defs ([Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    args0)
                     , Right (ClsInst
    inst, [Type]
    _) <- InstEnvs -> Class -> [Type] -> Either SDoc (ClsInst, [Type])
    lookupUniqueInstEnv InstEnvs
    ienv Class
    knN_cls [Type]
    args1
                     -> (ClsInst, Class, [Type], [Type])
    -> Maybe (ClsInst, Class, [Type], [Type])
    forall a. a -> Maybe a
    Just (ClsInst
    inst,Class
    knN_cls,[Type]
    args0,[Type]
    args1)
                     | TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == KnownNatDefs -> TyCon
    ordCondTyCon KnownNatDefs
    defs
                     , [Type
    _,Type
    cmpNat,TyConApp TyCon
    t1 [],TyConApp TyCon
    t2 [],TyConApp TyCon
    f1 []] <- [Type]
    args0
                     , TyConApp TyCon
    cmpNatTc args2 :: [Type]
    args2@(Type
    arg2:[Type]
    _) <- Type
    cmpNat
                     , TyCon
    cmpNatTc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    typeNatCmpTyCon
                     , TyCon
    t1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
                     , TyCon
    t2 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedTrueDataCon
                     , TyCon
    f1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    promotedFalseDataCon
                     , let knN_cls :: Class
    knN_cls = KnownNatDefs -> Class
    knownBoolNat2 KnownNatDefs
    defs
                           ki :: Type
    ki      = (() :: Constraint) => Type -> Type
    Type -> Type
    typeKind Type
    arg2
                           args1N :: [Type]
    args1N  = Type
    kiType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :Type
    fn1Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args2
                     , Right (ClsInst
    inst,[Type]
    _) <- InstEnvs -> Class -> [Type] -> Either SDoc (ClsInst, [Type])
    lookupUniqueInstEnv InstEnvs
    ienv Class
    knN_cls [Type]
    args1N
                     -> (ClsInst, Class, [Type], [Type])
    -> Maybe (ClsInst, Class, [Type], [Type])
    forall a. a -> Maybe a
    Just (ClsInst
    inst,Class
    knN_cls,[Type]
    args2,[Type]
    args1N)
                     | [Type
    arg0,Type
    _] <- [Type]
    args0
                     , let knN_cls :: Class
    knN_cls = KnownNatDefs -> Class
    knownBoolNat2 KnownNatDefs
    defs
                           ki :: Type
    ki      = (() :: Constraint) => Type -> Type
    Type -> Type
    typeKind Type
    arg0
                           args1N :: [Type]
    args1N  = Type
    kiType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args1
                     , Right (ClsInst
    inst, [Type]
    _) <- InstEnvs -> Class -> [Type] -> Either SDoc (ClsInst, [Type])
    lookupUniqueInstEnv InstEnvs
    ienv Class
    knN_cls [Type]
    args1N
                     -> (ClsInst, Class, [Type], [Type])
    -> Maybe (ClsInst, Class, [Type], [Type])
    forall a. a -> Maybe a
    Just (ClsInst
    inst,Class
    knN_cls,[Type]
    args0,[Type]
    args1N)
                     | (Type
    arg0:[Type]
    args0Rest) <- [Type]
    args0
                     , [Type] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Type]
    args0Rest Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    3
                     , TyCon
    tc TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == KnownNatDefs -> TyCon
    ifTyCon KnownNatDefs
    defs
                     , let args1N :: [Type]
    args1N = Type
    arg0Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :Type
    fn1Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args0Rest
                           knN_cls :: Class
    knN_cls = KnownNatDefs -> Class
    knownNat2Bool KnownNatDefs
    defs
                     , Right (ClsInst
    inst, [Type]
    _) <- InstEnvs -> Class -> [Type] -> Either SDoc (ClsInst, [Type])
    lookupUniqueInstEnv InstEnvs
    ienv Class
    knN_cls [Type]
    args1N
                     -> (ClsInst, Class, [Type], [Type])
    -> Maybe (ClsInst, Class, [Type], [Type])
    forall a. a -> Maybe a
    Just (ClsInst
    inst,Class
    knN_cls,[Type]
    args0Rest,[Type]
    args1N)
                     | Bool
    otherwise
                     -> Maybe (ClsInst, Class, [Type], [Type])
    forall a. Maybe a
    Nothing
            case Maybe (ClsInst, Class, [Type], [Type])
    instM of
              Just (ClsInst
    inst,Class
    knN_cls,[Type]
    args0N,[Type]
    args1N) -> do
                let df_id :: DFunId
    df_id   = ClsInst -> DFunId
    instanceDFunId ClsInst
    inst
                    df :: (Class, DFunId)
    df      = (Class
    knN_cls,DFunId
    df_id)
                    df_args :: [Scaled Type]
    df_args = ([Scaled Type], Type) -> [Scaled Type]
    forall a b. (a, b) -> a
    fst                  -- [KnownNat x, KnownNat y]

                            (([Scaled Type], Type) -> [Scaled Type])
    -> (Type -> ([Scaled Type], Type)) -> Type -> [Scaled Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ([Scaled Type], Type)
    splitFunTys          -- ([KnownNat x, KnowNat y], DKnownNat2 "+" x y)

                            (Type -> ([Scaled Type], Type))
    -> (Type -> Type) -> Type -> ([Scaled Type], Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((() :: Constraint) => Type -> [Type] -> Type
    Type -> [Type] -> Type
    `piResultTys` [Type]
    args0N) -- (KnowNat x, KnownNat y) => DKnownNat2 "+" x y

                            (Type -> [Scaled Type]) -> Type -> [Scaled Type]
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    df_id         -- forall a b . (KnownNat a, KnownNat b) => DKnownNat2 "+" a b

                ([EvExpr]
    evs,[[Ct]]
    new) <- [(EvExpr, [Ct])] -> ([EvExpr], [[Ct]])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(EvExpr, [Ct])] -> ([EvExpr], [[Ct]]))
    -> TcPluginM [(EvExpr, [Ct])] -> TcPluginM ([EvExpr], [[Ct]])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Scaled Type -> TcPluginM (EvExpr, [Ct]))
    -> [Scaled Type] -> TcPluginM [(EvExpr, [Ct])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Type -> TcPluginM (EvExpr, [Ct])
    go_arg (Type -> TcPluginM (EvExpr, [Ct]))
    -> (Scaled Type -> Type) -> Scaled Type -> TcPluginM (EvExpr, [Ct])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Scaled Type -> Type
    forall a. Scaled a -> a
    irrelevantMult) [Scaled Type]
    df_args
                if Class -> Name
    className Class
    cls Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Class -> Name
    className (KnownNatDefs -> Class
    knownBool KnownNatDefs
    defs)
                   -- Create evidence using the original, flattened, argument of

                   -- the KnownNat we're trying to solve. Not doing this results in

                   -- GHC panics for:

                   -- https://gist.github.com/christiaanb/0d204fe19f89b28f1f8d24feb63f1e63

                   --

                   -- That's because the flattened KnownNat we're asked to solve is

                   -- [W] KnownNat fsk

                   -- given:

                   -- [G] fsk ~ CLog 2 n + 1

                   -- [G] fsk2 ~ n

                   -- [G] fsk2 ~ n + m

                   --

                   -- Our flattening picks one of the solution, so we try to solve

                   -- [W] KnownNat (CLog 2 n + 1)

                   --

                   -- Turns out, GHC wanted us to solve:

                   -- [W] KnownNat (CLog 2 (n + m) + 1)

                   --

                   -- But we have no way of knowing this! Solving the "wrong" expansion

                   -- of 'fsk' results in:

                   --

                   -- ghc: panic! (the 'impossible' happened)

                   -- (GHC version 8.6.5 for x86_64-unknown-linux):

                   --       buildKindCoercion

                   -- CLog 2 (n_a681K + m_a681L)

                   -- CLog 2 n_a681K

                   -- n_a681K + m_a681L

                   -- n_a681K

                   --

                   -- down the line.

                   --

                   -- So while the "shape" of the KnownNat evidence that we return

                   -- follows 'CLog 2 n + 1', the type of the evidence will be

                   -- 'KnownNat fsk'; the one GHC originally asked us to solve.

                   then Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((,[[Ct]] -> [Ct]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Ct]]
    new) (EvTerm -> (EvTerm, [Ct])) -> Maybe EvTerm -> Maybe (EvTerm, [Ct])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Class, DFunId)
    -> Class -> [Type] -> [Type] -> Type -> [EvExpr] -> Maybe EvTerm
    makeOpDictByFiat (Class, DFunId)
    df Class
    cls [Type]
    args1N [Type]
    args0N (Orig Type -> Type
    forall a. Orig a -> a
    unOrig Orig Type
    orig) [EvExpr]
    evs)
                   else Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((,[[Ct]] -> [Ct]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Ct]]
    new) (EvTerm -> (EvTerm, [Ct])) -> Maybe EvTerm -> Maybe (EvTerm, [Ct])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Class, DFunId)
    -> Class
    -> [Type]
    -> [Type]
    -> Type
    -> [EvExpr]
    -> Maybe (Type, Coercion)
    -> Maybe EvTerm
    makeOpDict (Class, DFunId)
    df Class
    cls [Type]
    args1N [Type]
    args0N (Orig Type -> Type
    forall a. Orig a -> a
    unOrig Orig Type
    orig) [EvExpr]
    evs ((Coercion -> (Type, Coercion))
    -> Maybe Coercion -> Maybe (Type, Coercion)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Type
    ty,) Maybe Coercion
    sM))
              Maybe (ClsInst, Class, [Type], [Type])
    _ -> Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((,[]) (EvTerm -> (EvTerm, [Ct])) -> Maybe EvTerm -> Maybe (EvTerm, [Ct])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Maybe EvTerm
    go_other Type
    ty)

        go ((LitTy (NumTyLit Integer
    i)), Maybe Coercion
    _)
          -- Let GHC solve simple Literal constraints

          | LitTy TyLit
    _ <- Type
    op
          = Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (EvTerm, [Ct])
    forall a. Maybe a
    Nothing
          -- This plugin only solves Literal KnownNat's that needed to be normalised

          -- first

          | Bool
    otherwise
          = ((EvTerm -> (EvTerm, [Ct])) -> Maybe EvTerm -> Maybe (EvTerm, [Ct])
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (,[])) (Maybe EvTerm -> Maybe (EvTerm, [Ct]))
    -> TcPluginM (Maybe EvTerm) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Class -> Type -> Integer -> TcPluginM (Maybe EvTerm)
    makeLitDict Class
    cls Type
    op Integer
    i
        go (Type, Maybe Coercion)
    _ = Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (EvTerm, [Ct])
    forall a. Maybe a
    Nothing

        -- Get EvTerm arguments for type-level operations. If they do not exist

        -- as [G]iven constraints, then generate new [W]anted constraints

        go_arg :: PredType -> TcPluginM (EvExpr,[Ct])
        go_arg :: Type -> TcPluginM (EvExpr, [Ct])
    go_arg Type
    ty = case CType -> [(CType, EvExpr)] -> Maybe EvExpr
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (Type -> CType
    CType Type
    ty) [(CType, EvExpr)]
    givens of
          Just EvExpr
    ev -> (EvExpr, [Ct]) -> TcPluginM (EvExpr, [Ct])
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvExpr
    ev,[])
          Maybe EvExpr
    _ -> do
            (EvExpr
    ev,Ct
    wanted) <- Ct -> Type -> TcPluginM (EvExpr, Ct)
    makeWantedEv Ct
    ct Type
    ty
            (EvExpr, [Ct]) -> TcPluginM (EvExpr, [Ct])
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvExpr
    ev,[Ct
    wanted])

        -- Fall through case: look up the normalised [W]anted constraint in the list

        -- of [G]iven constraints.

        go_other :: Type -> Maybe EvTerm
        go_other :: Type -> Maybe EvTerm
    go_other Type
    ty =
          let knClsTc :: TyCon
    knClsTc = Class -> TyCon
    classTyCon Class
    cls
              kn :: Type
    kn      = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    knClsTc [Type
    ty]
              cast :: EvExpr -> Maybe EvTerm
    cast    = if Type -> CType
    CType Type
    ty CType -> CType -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type -> CType
    CType Type
    op
                           then EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just (EvTerm -> Maybe EvTerm)
    -> (EvExpr -> EvTerm) -> EvExpr -> Maybe EvTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EvExpr -> EvTerm
    EvExpr
                           else Class -> Type -> Type -> EvExpr -> Maybe EvTerm
    makeKnCoercion Class
    cls Type
    ty Type
    op
          in  EvExpr -> Maybe EvTerm
    cast (EvExpr -> Maybe EvTerm) -> Maybe EvExpr -> Maybe EvTerm
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< CType -> [(CType, EvExpr)] -> Maybe EvExpr
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (Type -> CType
    CType Type
    kn) [(CType, EvExpr)]
    givens

        -- Find a known constraint for a wanted, so that (modulo normalization)

        -- the two are a constant offset apart.

        offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))
        offset :: Type -> TcPluginM (Maybe (EvTerm, [Ct]))
    offset LitTy{} = Maybe (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (EvTerm, [Ct])
    forall a. Maybe a
    Nothing
        offset Type
    want = MaybeT TcPluginM (EvTerm, [Ct]) -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT TcPluginM (EvTerm, [Ct])
     -> TcPluginM (Maybe (EvTerm, [Ct])))
    -> MaybeT TcPluginM (EvTerm, [Ct])
    -> TcPluginM (Maybe (EvTerm, [Ct]))
    forall a b. (a -> b) -> a -> b
    $ do
          let -- Get the knownnat contraints

              unKn :: Type -> Maybe Type
    unKn Type
    ty' = case Type -> Pred
    classifyPredType Type
    ty' of
                           ClassPred Class
    cls' [Type
    ty'']
                             | Class -> Name
    className Class
    cls' Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    knownNatClassName
                             -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    ty''
                           Pred
    _ -> Maybe Type
    forall a. Maybe a
    Nothing
              -- Get the rewrites

              unEq :: (Type, c) -> Maybe (Type, Type, c)
    unEq (Type
    ty',c
    ev) = case Type -> Pred
    classifyPredType Type
    ty' of
                                EqPred EqRel
    NomEq Type
    ty1 Type
    ty2 -> (Type, Type, c) -> Maybe (Type, Type, c)
    forall a. a -> Maybe a
    Just (Type
    ty1,Type
    ty2,c
    ev)
                                Pred
    _ -> Maybe (Type, Type, c)
    forall a. Maybe a
    Nothing
              rewrites :: [(Type,Type,EvExpr)]
              rewrites :: [(Type, Type, EvExpr)]
    rewrites = ((CType, EvExpr) -> Maybe (Type, Type, EvExpr))
    -> [(CType, EvExpr)] -> [(Type, Type, EvExpr)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((Type, EvExpr) -> Maybe (Type, Type, EvExpr)
    forall {c}. (Type, c) -> Maybe (Type, Type, c)
    unEq ((Type, EvExpr) -> Maybe (Type, Type, EvExpr))
    -> ((CType, EvExpr) -> (Type, EvExpr))
    -> (CType, EvExpr)
    -> Maybe (Type, Type, EvExpr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CType -> Type) -> (CType, EvExpr) -> (Type, EvExpr)
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first CType -> Type
    unCType) [(CType, EvExpr)]
    givens
              -- Rewrite

              rewriteTy :: Type
    -> (Type, Type, EvExpr)
    -> Maybe (Type, Maybe (Type, Maybe Coercion))
    rewriteTy Type
    tyK (Type
    ty1,Type
    ty2,EvExpr
    ev)
                | Type
    ty1 Type -> Type -> Bool
    `eqType` Type
    tyK
                = (Type, Maybe (Type, Maybe Coercion))
    -> Maybe (Type, Maybe (Type, Maybe Coercion))
    forall a. a -> Maybe a
    Just (Type
    ty2,(Type, Maybe Coercion) -> Maybe (Type, Maybe Coercion)
    forall a. a -> Maybe a
    Just (Type
    tyK,EvTerm -> Maybe Coercion
    evTermCoercion_maybe (EvExpr -> EvTerm
    EvExpr EvExpr
    ev)))
                | Type
    ty2 Type -> Type -> Bool
    `eqType` Type
    tyK
                = (Type, Maybe (Type, Maybe Coercion))
    -> Maybe (Type, Maybe (Type, Maybe Coercion))
    forall a. a -> Maybe a
    Just (Type
    ty1,(Type, Maybe Coercion) -> Maybe (Type, Maybe Coercion)
    forall a. a -> Maybe a
    Just (Type
    tyK,(Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Coercion -> Coercion
    mkTcSymCo (EvTerm -> Maybe Coercion
    evTermCoercion_maybe (EvExpr -> EvTerm
    EvExpr EvExpr
    ev))))
                | Bool
    otherwise
                = Maybe (Type, Maybe (Type, Maybe Coercion))
    forall a. Maybe a
    Nothing
              -- Get only the [G]iven KnownNat constraints

              knowns :: [Type]
    knowns   = ((CType, EvExpr) -> Maybe Type) -> [(CType, EvExpr)] -> [Type]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (Type -> Maybe Type
    unKn (Type -> Maybe Type)
    -> ((CType, EvExpr) -> Type) -> (CType, EvExpr) -> Maybe Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CType -> Type
    unCType (CType -> Type)
    -> ((CType, EvExpr) -> CType) -> (CType, EvExpr) -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (CType, EvExpr) -> CType
    forall a b. (a, b) -> a
    fst) [(CType, EvExpr)]
    givens
              -- Get all the rewritten KNs

              knownsR :: [(Type, Maybe (Type, Maybe Coercion))]
    knownsR  = [Maybe (Type, Maybe (Type, Maybe Coercion))]
    -> [(Type, Maybe (Type, Maybe Coercion))]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Type, Maybe (Type, Maybe Coercion))]
     -> [(Type, Maybe (Type, Maybe Coercion))])
    -> [Maybe (Type, Maybe (Type, Maybe Coercion))]
    -> [(Type, Maybe (Type, Maybe Coercion))]
    forall a b. (a -> b) -> a -> b
    $ (Type -> [Maybe (Type, Maybe (Type, Maybe Coercion))])
    -> [Type] -> [Maybe (Type, Maybe (Type, Maybe Coercion))]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\Type
    t -> ((Type, Type, EvExpr)
     -> Maybe (Type, Maybe (Type, Maybe Coercion)))
    -> [(Type, Type, EvExpr)]
    -> [Maybe (Type, Maybe (Type, Maybe Coercion))]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type
    -> (Type, Type, EvExpr)
    -> Maybe (Type, Maybe (Type, Maybe Coercion))
    rewriteTy Type
    t) [(Type, Type, EvExpr)]
    rewrites) [Type]
    knowns
              knownsX :: [(Type, Maybe (Type, Maybe Coercion))]
              knownsX :: [(Type, Maybe (Type, Maybe Coercion))]
    knownsX  = (Type -> (Type, Maybe (Type, Maybe Coercion)))
    -> [Type] -> [(Type, Maybe (Type, Maybe Coercion))]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (,Maybe (Type, Maybe Coercion)
    forall a. Maybe a
    Nothing) [Type]
    knowns [(Type, Maybe (Type, Maybe Coercion))]
    -> [(Type, Maybe (Type, Maybe Coercion))]
    -> [(Type, Maybe (Type, Maybe Coercion))]
    forall a. [a] -> [a] -> [a]
    ++ [(Type, Maybe (Type, Maybe Coercion))]
    knownsR
              -- pair up the sum-of-products KnownNat constraints

              -- with the original Nat operation

              subWant :: Type -> Type
    subWant  = TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon ([Type] -> Type) -> (Type -> [Type]) -> Type -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type
    want])
              -- exploded :: [()]

              exploded :: [(CoreSOP, (Type, Maybe (Type, Maybe Coercion)))]
    exploded = ((Type, Maybe (Type, Maybe Coercion))
     -> (CoreSOP, (Type, Maybe (Type, Maybe Coercion))))
    -> [(Type, Maybe (Type, Maybe Coercion))]
    -> [(CoreSOP, (Type, Maybe (Type, Maybe Coercion)))]
    forall a b. (a -> b) -> [a] -> [b]
    map ((CoreSOP, [(Type, Type)]) -> CoreSOP
    forall a b. (a, b) -> a
    fst ((CoreSOP, [(Type, Type)]) -> CoreSOP)
    -> ((Type, Maybe (Type, Maybe Coercion))
        -> (CoreSOP, [(Type, Type)]))
    -> (Type, Maybe (Type, Maybe Coercion))
    -> CoreSOP
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
    forall w a. Writer w a -> (a, w)
    runWriter (Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)]))
    -> ((Type, Maybe (Type, Maybe Coercion))
        -> Writer [(Type, Type)] CoreSOP)
    -> (Type, Maybe (Type, Maybe Coercion))
    -> (CoreSOP, [(Type, Type)])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Writer [(Type, Type)] CoreSOP
    normaliseNat (Type -> Writer [(Type, Type)] CoreSOP)
    -> ((Type, Maybe (Type, Maybe Coercion)) -> Type)
    -> (Type, Maybe (Type, Maybe Coercion))
    -> Writer [(Type, Type)] CoreSOP
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Type
    subWant (Type -> Type)
    -> ((Type, Maybe (Type, Maybe Coercion)) -> Type)
    -> (Type, Maybe (Type, Maybe Coercion))
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type, Maybe (Type, Maybe Coercion)) -> Type
    forall a b. (a, b) -> a
    fst ((Type, Maybe (Type, Maybe Coercion)) -> CoreSOP)
    -> ((Type, Maybe (Type, Maybe Coercion))
        -> (Type, Maybe (Type, Maybe Coercion)))
    -> (Type, Maybe (Type, Maybe Coercion))
    -> (CoreSOP, (Type, Maybe (Type, Maybe Coercion)))
    forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
    forall (a :: * -> * -> *) b c c'.
    Arrow a =>
    a b c -> a b c' -> a b (c, c')
    &&& (Type, Maybe (Type, Maybe Coercion))
    -> (Type, Maybe (Type, Maybe Coercion))
    forall a. a -> a
    id)
                             [(Type, Maybe (Type, Maybe Coercion))]
    knownsX
              -- interesting cases for us are those where

              -- wanted and given only differ by a constant

              examineDiff :: SOP v c -> a -> Maybe (a, Symbol v c)
    examineDiff (S [P [I Integer
    n]]) a
    entire = (a, Symbol v c) -> Maybe (a, Symbol v c)
    forall a. a -> Maybe a
    Just (a
    entire,Integer -> Symbol v c
    forall v c. Integer -> Symbol v c
    I Integer
    n)
              examineDiff (S [P [V v
    v]]) a
    entire = (a, Symbol v c) -> Maybe (a, Symbol v c)
    forall a. a -> Maybe a
    Just (a
    entire,v -> Symbol v c
    forall v c. v -> Symbol v c
    V v
    v)
              examineDiff SOP v c
    _ a
    _ = Maybe (a, Symbol v c)
    forall a. Maybe a
    Nothing
              interesting :: [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c)]
    interesting = ((CoreSOP, (Type, Maybe (Type, Maybe Coercion)))
     -> Maybe ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c))
    -> [(CoreSOP, (Type, Maybe (Type, Maybe Coercion)))]
    -> [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((CoreSOP
     -> (Type, Maybe (Type, Maybe Coercion))
     -> Maybe ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c))
    -> (CoreSOP, (Type, Maybe (Type, Maybe Coercion)))
    -> Maybe ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry CoreSOP
    -> (Type, Maybe (Type, Maybe Coercion))
    -> Maybe ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c)
    forall {v} {c} {a} {c}. SOP v c -> a -> Maybe (a, Symbol v c)
    examineDiff) [(CoreSOP, (Type, Maybe (Type, Maybe Coercion)))]
    exploded
          -- convert the first suitable evidence

          (((Type
    h,Maybe (Type, Maybe Coercion)
    sM),Symbol DFunId CType
    corr):[((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType)]
    _) <- [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType)]
    -> MaybeT
         TcPluginM
         [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType)]
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType)]
    forall {c}.
    [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c)]
    interesting
          (Type, Maybe Coercion)
    x <- case Symbol DFunId CType
    corr of
                    I Integer
    0 -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Type, Maybe Coercion)
    -> Maybe (Type, Maybe Coercion) -> (Type, Maybe Coercion)
    forall a. a -> Maybe a -> a
    fromMaybe (Type
    h,Maybe Coercion
    forall a. Maybe a
    Nothing) Maybe (Type, Maybe Coercion)
    sM)
                    I Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0
                        , let l1 :: Type
    l1 = Integer -> Type
    mkNumLitTy (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    i)
                        -> case Maybe (Type, Maybe Coercion)
    sM of
                            Just (Type
    q,Maybe Coercion
    cM) -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatAddTyCon [Type
    q,Type
    l1]
                              , (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    typeNatAddTyCon ([Coercion] -> Coercion)
    -> (Coercion -> [Coercion]) -> Coercion -> Coercion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Coercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Type -> Coercion
    mkNomReflCo Type
    l1])) Maybe Coercion
    cM
                              )
                            Maybe (Type, Maybe Coercion)
    Nothing -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatAddTyCon [Type
    h,Type
    l1]
                              , Maybe Coercion
    forall a. Maybe a
    Nothing
                              )
                        | Bool
    otherwise
                        , let l1 :: Type
    l1 = Integer -> Type
    mkNumLitTy Integer
    i
                        -> case Maybe (Type, Maybe Coercion)
    sM of
                            Just (Type
    q,Maybe Coercion
    cM) -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    q,Type
    l1]
                              , (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    typeNatSubTyCon ([Coercion] -> Coercion)
    -> (Coercion -> [Coercion]) -> Coercion -> Coercion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Coercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Type -> Coercion
    mkNomReflCo Type
    l1])) Maybe Coercion
    cM
                              )
                            Maybe (Type, Maybe Coercion)
    Nothing -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    h,Type
    l1]
                              , Maybe Coercion
    forall a. Maybe a
    Nothing
                              )
                    -- If the offset between a given and a wanted is again the wanted

                    -- then the given is twice the wanted; so we can just divide

                    -- the given by two. Only possible in GHC 8.4+; for 8.2 we simply

                    -- fail because we don't know how to divide.

                    Symbol DFunId CType
    c   | Type -> CType
    CType (CoreSOP -> Type
    reifySOP ([Product DFunId CType] -> CoreSOP
    forall v c. [Product v c] -> SOP v c
    S [[Symbol DFunId CType] -> Product DFunId CType
    forall v c. [Symbol v c] -> Product v c
    P [Symbol DFunId CType
    c]])) CType -> CType -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type -> CType
    CType Type
    want
                        , let l2 :: Type
    l2 = Integer -> Type
    mkNumLitTy Integer
    2
                        -> case Maybe (Type, Maybe Coercion)
    sM of
                            Just (Type
    q,Maybe Coercion
    cM) -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatDivTyCon [Type
    q,Type
    l2]
                              , (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    typeNatDivTyCon ([Coercion] -> Coercion)
    -> (Coercion -> [Coercion]) -> Coercion -> Coercion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Coercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Type -> Coercion
    mkNomReflCo Type
    l2])) Maybe Coercion
    cM
                              )
                            Maybe (Type, Maybe Coercion)
    Nothing -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                              ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatDivTyCon [Type
    h,Type
    l2]
                              , Maybe Coercion
    forall a. Maybe a
    Nothing
                              )
                    -- Only solve with a variable offset if we have [G]iven knownnat for it

                    -- Failing to do this check results in #30

                    V DFunId
    v  | ((Type, Maybe (Type, Maybe Coercion)) -> Bool)
    -> [(Type, Maybe (Type, Maybe Coercion))] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Bool -> Bool
    not (Bool -> Bool)
    -> ((Type, Maybe (Type, Maybe Coercion)) -> Bool)
    -> (Type, Maybe (Type, Maybe Coercion))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Type -> Bool
    eqType (DFunId -> Type
    TyVarTy DFunId
    v) (Type -> Bool)
    -> ((Type, Maybe (Type, Maybe Coercion)) -> Type)
    -> (Type, Maybe (Type, Maybe Coercion))
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type, Maybe (Type, Maybe Coercion)) -> Type
    forall a b. (a, b) -> a
    fst) [(Type, Maybe (Type, Maybe Coercion))]
    knownsX
                         -> TcPluginM (Maybe (Type, Maybe Coercion))
    -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (Maybe (Type, Maybe Coercion)
    -> TcPluginM (Maybe (Type, Maybe Coercion))
    forall a. a -> TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (Type, Maybe Coercion)
    forall a. Maybe a
    Nothing)
                    Symbol DFunId CType
    _    -> let lC :: Type
    lC = CoreSOP -> Type
    reifySOP ([Product DFunId CType] -> CoreSOP
    forall v c. [Product v c] -> SOP v c
    S [[Symbol DFunId CType] -> Product DFunId CType
    forall v c. [Symbol v c] -> Product v c
    P [Symbol DFunId CType
    corr]]) in
                            case Maybe (Type, Maybe Coercion)
    sM of
                              Just (Type
    q,Maybe Coercion
    cM) -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                                ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    q,Type
    lC]
                                , (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Nominal TyCon
    typeNatSubTyCon ([Coercion] -> Coercion)
    -> (Coercion -> [Coercion]) -> Coercion -> Coercion
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Coercion -> [Coercion] -> [Coercion]
    forall a. a -> [a] -> [a]
    :[Type -> Coercion
    mkNomReflCo Type
    lC])) Maybe Coercion
    cM
                                )
                              Maybe (Type, Maybe Coercion)
    Nothing -> (Type, Maybe Coercion) -> MaybeT TcPluginM (Type, Maybe Coercion)
    forall a. a -> MaybeT TcPluginM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                                ( TyCon -> [Type] -> Type
    mkTyConApp TyCon
    typeNatSubTyCon [Type
    h,Type
    lC]
                                , Maybe Coercion
    forall a. Maybe a
    Nothing
                                )
          TcPluginM (Maybe (EvTerm, [Ct])) -> MaybeT TcPluginM (EvTerm, [Ct])
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT ((Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm, [Ct]))
    go (Type, Maybe Coercion)
    x)

    makeWantedEv
      :: Ct
      -> Type
      -> TcPluginM (EvExpr,Ct)
    makeWantedEv :: Ct -> Type -> TcPluginM (EvExpr, Ct)
    makeWantedEv Ct
    ct Type
    ty = do
      -- Create a new wanted constraint

      CtEvidence
    wantedCtEv <- CtLoc -> Type -> TcPluginM CtEvidence
    newWanted (Ct -> CtLoc
    ctLoc Ct
    ct) Type
    ty
      let ev :: EvExpr
    ev      = (() :: Constraint) => CtEvidence -> EvExpr
    CtEvidence -> EvExpr
    ctEvExpr CtEvidence
    wantedCtEv
          wanted :: Ct
    wanted  = CtEvidence -> Ct
    mkNonCanonical CtEvidence
    wantedCtEv
      (EvExpr, Ct) -> TcPluginM (EvExpr, Ct)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvExpr
    ev,Ct
    wanted)

    {- |
    Given:

    * A "magic" class, and corresponding instance dictionary function, for a
      type-level arithmetic operation
    * Two KnownNat dictionaries

    makeOpDict instantiates the dictionary function with the KnownNat dictionaries,
    and coerces it to a KnownNat dictionary. i.e. for KnownNat2, the "magic"
    dictionary for binary functions, the coercion happens in the following steps:

    1. KnownNat2 "+" a b           -> SNatKn (KnownNatF2 "+" a b)
    2. SNatKn (KnownNatF2 "+" a b) -> Integer
    3. Integer                     -> SNat (a + b)
    4. SNat (a + b)                -> KnownNat (a + b)

    this process is mirrored for the dictionary functions of a higher arity
    -}
    makeOpDict
      :: (Class,DFunId)
      -- ^ "magic" class function and dictionary function id

      -> Class
      -- ^ KnownNat class

      -> [Type]
      -- ^ Argument types for the Class

      -> [Type]
      -- ^ Argument types for the Instance

      -> Type
      -- ^ Type of the result

      -> [EvExpr]
      -- ^ Evidence arguments

      -> Maybe (Type, Coercion)
      -> Maybe EvTerm
    makeOpDict :: (Class, DFunId)
    -> Class
    -> [Type]
    -> [Type]
    -> Type
    -> [EvExpr]
    -> Maybe (Type, Coercion)
    -> Maybe EvTerm
    makeOpDict (Class
    opCls,DFunId
    dfid) Class
    knCls [Type]
    tyArgsC [Type]
    tyArgsI Type
    z [EvExpr]
    evArgs Maybe (Type, Coercion)
    sM
      | let z1 :: Type
    z1 = Type
    -> ((Type, Coercion) -> Type) -> Maybe (Type, Coercion) -> Type
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Type
    z (Type, Coercion) -> Type
    forall a b. (a, b) -> a
    fst Maybe (Type, Coercion)
    sM
      , Just (Type
    _, Coercion
    kn_co_dict) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    knCls) [Type
    z1]
        -- KnownNat n ~ SNat n

      , [ DFunId
    kn_meth ] <- Class -> [DFunId]
    classMethods Class
    knCls
      , Just TyCon
    kn_tcRep <- Type -> Maybe TyCon
    tyConAppTyCon_maybe -- SNat

                          (Type -> Maybe TyCon) -> Type -> Maybe TyCon
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy      -- SNat n

                          (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type
    dropForAlls      -- KnownNat n => SNat n

                          (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    kn_meth   -- forall n. KnownNat n => SNat n

      , Just (Type
    _, Coercion
    kn_co_rep) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    kn_tcRep [Type
    z1]
        -- SNat n ~ Integer

      , Just (Type
    _, Coercion
    op_co_dict) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    opCls) [Type]
    tyArgsC
        -- KnownNatAdd a b ~ SNatKn (a+b)

      , [ DFunId
    op_meth ] <- Class -> [DFunId]
    classMethods Class
    opCls
      , Just (TyCon
    op_tcRep,[Type]
    op_args) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe        -- (SNatKn, [KnownNatF2 f x y])

                                     (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy            -- SNatKn (KnownNatF2 f x y)

                                     (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ ((() :: Constraint) => Type -> [Type] -> Type
    Type -> [Type] -> Type
    `piResultTys` [Type]
    tyArgsC) -- KnownNatAdd f x y => SNatKn (KnownNatF2 f x y)

                                     (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    op_meth         -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b)

      , Just (Type
    _, Coercion
    op_co_rep) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    op_tcRep [Type]
    op_args
        -- SNatKn (a+b) ~ Integer

      , EvExpr EvExpr
    dfun_inst <- DFunId -> [Type] -> [EvExpr] -> EvTerm
    evDFunApp DFunId
    dfid [Type]
    tyArgsI [EvExpr]
    evArgs
            -- KnownNatAdd a b

      , let op_to_kn :: Coercion
    op_to_kn  = Coercion -> Coercion -> Coercion
    mkTcTransCo (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    op_co_dict Coercion
    op_co_rep)
                                    (Coercion -> Coercion
    mkTcSymCo (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    kn_co_dict Coercion
    kn_co_rep))
            -- KnownNatAdd a b ~ KnownNat (a+b)

      , let op_to_kn1 :: Coercion
    op_to_kn1 = case Maybe (Type, Coercion)
    sM of
              Maybe (Type, Coercion)
    Nothing -> Coercion
    op_to_kn
              Just (Type
    _,Coercion
    rw) ->
                let kn_co_rw :: Coercion
    kn_co_rw = (() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
    Role -> TyCon -> [Coercion] -> Coercion
    mkTyConAppCo Role
    Representational (Class -> TyCon
    classTyCon Class
    knCls) [Coercion
    rw]
                    kn_co_co :: Coercion
    kn_co_co = UnivCoProvenance -> Role -> Type -> Type -> Coercion
    mkUnivCo (CommandLineOption -> UnivCoProvenance
    PluginProv CommandLineOption
    "ghc-typelits-knownnat")
                                Role
    Representational
                                  (Coercion -> Type
    coercionRKind Coercion
    kn_co_rw)
                                  (TyCon -> [Type] -> Type
    mkTyConApp (Class -> TyCon
    classTyCon Class
    knCls) [Type
    z])
                  in Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    op_to_kn (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    kn_co_rw Coercion
    kn_co_co)
      , let ev_tm :: EvTerm
    ev_tm = EvExpr -> Coercion -> EvTerm
    mkEvCast EvExpr
    dfun_inst Coercion
    op_to_kn1
      = EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just EvTerm
    ev_tm
      | Bool
    otherwise
      = Maybe EvTerm
    forall a. Maybe a
    Nothing

    {-
    Given:
    * A KnownNat dictionary evidence over a type x
    * a desired type z
    makeKnCoercion assembles a coercion from a KnownNat x
    dictionary to a KnownNat z dictionary and applies it
    to the passed-in evidence.
    The coercion happens in the following steps:
    1. KnownNat x -> SNat x
    2. SNat x     -> Integer
    3. Integer    -> SNat z
    4. SNat z     -> KnownNat z
    -}
    makeKnCoercion :: Class          -- ^ KnownNat class

                   -> Type           -- ^ Type of the argument

                   -> Type           -- ^ Type of the result

                   -> EvExpr
                   -- ^ KnownNat dictionary for the argument

                   -> Maybe EvTerm
    makeKnCoercion :: Class -> Type -> Type -> EvExpr -> Maybe EvTerm
    makeKnCoercion Class
    knCls Type
    x Type
    z EvExpr
    xEv
      | Just (Type
    _, Coercion
    kn_co_dict_z) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    knCls) [Type
    z]
        -- KnownNat z ~ SNat z

      , [ DFunId
    kn_meth ] <- Class -> [DFunId]
    classMethods Class
    knCls
      , Just TyCon
    kn_tcRep <- Type -> Maybe TyCon
    tyConAppTyCon_maybe -- SNat

                          (Type -> Maybe TyCon) -> Type -> Maybe TyCon
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy      -- SNat n

                          (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type
    dropForAlls      -- KnownNat n => SNat n

                          (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    kn_meth   -- forall n. KnownNat n => SNat n

      , Just (Type
    _, Coercion
    kn_co_rep_z) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    kn_tcRep [Type
    z]
        -- SNat z ~ Integer

      , Just (Type
    _, Coercion
    kn_co_rep_x) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    kn_tcRep [Type
    x]
        -- Integer ~ SNat x

      , Just (Type
    _, Coercion
    kn_co_dict_x) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    knCls) [Type
    x]
        -- SNat x ~ KnownNat x

      = EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just (EvTerm -> Maybe EvTerm)
    -> (Coercion -> EvTerm) -> Coercion -> Maybe EvTerm
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EvExpr -> Coercion -> EvTerm
    mkEvCast EvExpr
    xEv (Coercion -> Maybe EvTerm) -> Coercion -> Maybe EvTerm
    forall a b. (a -> b) -> a -> b
    $ (Coercion
    kn_co_dict_x Coercion -> Coercion -> Coercion
    `mkTcTransCo` Coercion
    kn_co_rep_x) Coercion -> Coercion -> Coercion
    `mkTcTransCo` Coercion -> Coercion
    mkTcSymCo (Coercion
    kn_co_dict_z Coercion -> Coercion -> Coercion
    `mkTcTransCo` Coercion
    kn_co_rep_z)
      | Bool
    otherwise = Maybe EvTerm
    forall a. Maybe a
    Nothing

    -- | THIS CODE IS COPIED FROM:

    -- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973

    --

    -- makeLitDict adds a coercion that will convert the literal into a dictionary

    -- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]

    -- in TcEvidence.  The coercion happens in 2 steps:

    --

    --     Integer -> SNat n     -- representation of literal to singleton

    --     SNat n  -> KnownNat n -- singleton to dictionary

    makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm)
    makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm)
    makeLitDict Class
    clas Type
    ty Integer
    i
      | Just (Type
    _, Coercion
    co_dict) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    clas) [Type
    ty]
        -- co_dict :: KnownNat n ~ SNat n

      , [ DFunId
    meth ]   <- Class -> [DFunId]
    classMethods Class
    clas
      , Just TyCon
    tcRep <- Type -> Maybe TyCon
    tyConAppTyCon_maybe -- SNat

                        (Type -> Maybe TyCon) -> Type -> Maybe TyCon
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy     -- SNat n

                        (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type
    dropForAlls     -- KnownNat n => SNat n

                        (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    meth     -- forall n. KnownNat n => SNat n

      , Just (Type
    _, Coercion
    co_rep) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    tcRep [Type
    ty]
            -- SNat n ~ Integer

      = do
        Platform
    platform <- TcM Platform -> TcPluginM Platform
    forall a. TcM a -> TcPluginM a
    unsafeTcPluginTcM TcM Platform
    forall a b. TcRnIf a b Platform
    getPlatform
        let et :: EvExpr
    et = Platform -> Integer -> EvExpr
    mkNaturalExpr Platform
    platform Integer
    i
            ev_tm :: EvTerm
    ev_tm = EvExpr -> Coercion -> EvTerm
    mkEvCast EvExpr
    et (Coercion -> Coercion
    mkTcSymCo (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    co_dict Coercion
    co_rep))
        Maybe EvTerm -> TcPluginM (Maybe EvTerm)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just EvTerm
    ev_tm)
      | Bool
    otherwise
      = Maybe EvTerm -> TcPluginM (Maybe EvTerm)
    forall a. a -> TcPluginM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe EvTerm
    forall a. Maybe a
    Nothing

    {- |
    Given:

    * A "magic" class, and corresponding instance dictionary function, for a
      type-level boolean operation
    * Two KnownBool dictionaries

    makeOpDictByFiat instantiates the dictionary function with the KnownBool
    dictionaries, and coerces it to a KnownBool dictionary. i.e. for KnownBoolNat2,
    the "magic" dictionary for binary functions, the coercion happens in the
    following steps:

    1. KnownBoolNat2 "<=?" x y     -> SBoolF "<=?"
    2. SBoolF "<=?"                -> Bool
    3. Bool                        -> SNat (x <=? y)  THE BY FIAT PART!
    4. SBool (x <=? y)             -> KnownBool (x <=? y)

    this process is mirrored for the dictionary functions of a higher arity
    -}
    makeOpDictByFiat
      :: (Class,DFunId)
      -- ^ "magic" class function and dictionary function id

      -> Class
       -- ^ KnownNat class

      -> [Type]
      -- ^ Argument types for the Class

      -> [Type]
      -- ^ Argument types for the Instance

      -> Type
      -- ^ Type of the result

      -> [EvExpr]
      -- ^ Evidence arguments

      -> Maybe EvTerm
    makeOpDictByFiat :: (Class, DFunId)
    -> Class -> [Type] -> [Type] -> Type -> [EvExpr] -> Maybe EvTerm
    makeOpDictByFiat (Class
    opCls,DFunId
    dfid) Class
    knCls [Type]
    tyArgsC [Type]
    tyArgsI Type
    z [EvExpr]
    evArgs
        -- KnownBool b ~ SBool b

      | Just (Type
    _, Coercion
    kn_co_dict) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    knCls) [Type
    z]
      , [ DFunId
    kn_meth ] <- Class -> [DFunId]
    classMethods Class
    knCls
      , Just TyCon
    kn_tcRep <- Type -> Maybe TyCon
    tyConAppTyCon_maybe -- SBool

                           (Type -> Maybe TyCon) -> Type -> Maybe TyCon
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy     -- SBool b

                           (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type
    dropForAlls     -- KnownBool b => SBool b

                           (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    kn_meth  -- forall b. KnownBool b => SBool b

        -- SBool b R~ Bool (The "Lie")

      , let kn_co_rep :: Coercion
    kn_co_rep = UnivCoProvenance -> Role -> Type -> Type -> Coercion
    mkUnivCo (CommandLineOption -> UnivCoProvenance
    PluginProv CommandLineOption
    "ghc-typelits-knownnat")
                                 Role
    Representational
                                 (TyCon -> [Type] -> Type
    mkTyConApp TyCon
    kn_tcRep [Type
    z]) Type
    boolTy
        -- KnownBoolNat2 f a b ~ SBool f

      , Just (Type
    _, Coercion
    op_co_dict) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe (Class -> TyCon
    classTyCon Class
    opCls) [Type]
    tyArgsC
      , [ DFunId
    op_meth ] <- Class -> [DFunId]
    classMethods Class
    opCls
      , Just (TyCon
    op_tcRep,[Type]
    op_args) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
    Type -> Maybe (TyCon, [Type])
    splitTyConApp_maybe        -- (SBool, [f])

                                     (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
    forall a b. (a -> b) -> a -> b
    $ (() :: Constraint) => Type -> Type
    Type -> Type
    funResultTy            -- SBool f

                                     (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ ((() :: Constraint) => Type -> [Type] -> Type
    Type -> [Type] -> Type
    `piResultTys` [Type]
    tyArgsC) -- KnownBoolNat2 f x y => SBool f

                                     (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ DFunId -> Type
    idType DFunId
    op_meth         -- forall f x y . KnownBoolNat2 f a b => SBoolf f

        -- SBoolF f ~ Bool

      , Just (Type
    _, Coercion
    op_co_rep) <- TyCon -> [Type] -> Maybe (Type, Coercion)
    tcInstNewTyCon_maybe TyCon
    op_tcRep [Type]
    op_args
      , EvExpr EvExpr
    dfun_inst <- DFunId -> [Type] -> [EvExpr] -> EvTerm
    evDFunApp DFunId
    dfid [Type]
    tyArgsI [EvExpr]
    evArgs
        -- KnownBoolNat2 f x y ~ KnownBool b

      , let op_to_kn :: Coercion
    op_to_kn  = Coercion -> Coercion -> Coercion
    mkTcTransCo (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    op_co_dict Coercion
    op_co_rep)
                                    (Coercion -> Coercion
    mkTcSymCo (Coercion -> Coercion -> Coercion
    mkTcTransCo Coercion
    kn_co_dict Coercion
    kn_co_rep))
            ev_tm :: EvTerm
    ev_tm     = EvExpr -> Coercion -> EvTerm
    mkEvCast EvExpr
    dfun_inst Coercion
    op_to_kn
      = EvTerm -> Maybe EvTerm
    forall a. a -> Maybe a
    Just EvTerm
    ev_tm
      | Bool
    otherwise
      = Maybe EvTerm
    forall a. Maybe a
    Nothing