{-|
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 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,mapMaybe)
import GHC.TcPluginM.Extra (lookupModule, lookupName, 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 (Role (Representational), 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)
import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), getPlatform)
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)
import GHC.Plugins
  (Coercion, mkSymCo, mkTransCo)
#else
import GHC.Tc.Types.Evidence
  (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)
#endif
import GHC.Types.Id (idType)
import GHC.Types.Name (nameModule_maybe, nameOccName)
import GHC.Types.Name.Occurrence (mkTcOcc, occNameString)
import GHC.Types.Unique.FM (emptyUFM)
import GHC.Types.Var (DFunId)
import GHC.Unit.Module (mkModuleName, moduleName, moduleNameString)

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

mkTcTransCo :: Coercion -> Coercion -> Coercion
mkTcTransCo = 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}
  }

-- | 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 :: TcPlugin
tcPlugin = Maybe TcPlugin -> TcPlugin
forall a b. a -> b -> a
const (Maybe TcPlugin -> TcPlugin) -> Maybe TcPlugin -> TcPlugin
forall a b. (a -> b) -> a -> b
$ TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just TcPlugin
normalisePlugin
#if MIN_VERSION_ghc(8,6,0)
  , pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = [CommandLineOption] -> IO 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
    Module
md     <- ModuleName -> FastString -> TcPluginM Module
lookupModule ModuleName
myModule FastString
myPackage
    Class
kbC    <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownBool"
    Class
kbn2C  <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownBoolNat2"
    Class
kn2bC  <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownNat2Bool"
    Class
kn1C   <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownNat1"
    Class
kn2C   <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownNat2"
    Class
kn3C   <- Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
"KnownNat3"
    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
                                   }
           }
  where
    look :: Module -> CommandLineOption -> TcPluginM Class
look Module
md CommandLineOption
s = do
      Name
nm   <- Module -> OccName -> TcPluginM Name
lookupName Module
md (CommandLineOption -> OccName
mkTcOcc CommandLineOption
s)
      Name -> TcPluginM Class
tcLookupClass Name
nm

    myModule :: ModuleName
myModule  = CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"GHC.TypeLits.KnownNat"
    myPackage :: FastString
myPackage = CommandLineOption -> FastString
fsLit CommandLineOption
"ghc-typelits-knownnat"

-- | 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 -> TcPluginM (Maybe (EvTerm, [Ct]))
go Type
op
    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 -> TcPluginM (Maybe (EvTerm,[Ct]))
    go :: Type -> TcPluginM (Maybe (EvTerm, [Ct]))
go (Type -> Maybe EvTerm
go_other -> Just EvTerm
ev) = 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)
      | 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)
                 | CommandLineOption
fn0 CommandLineOption -> CommandLineOption -> Bool
forall a. Eq a => a -> a -> Bool
== CommandLineOption
"Data.Type.Ord.OrdCond"
                 , [Type
_,Type
cmpNat,TyConApp TyCon
t1 [],TyConApp TyCon
t2 [],TyConApp TyCon
f1 []] <- [Type]
args0
                 , TyConApp TyCon
cmpNatTc [Type]
args2 <- 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] -> Type
forall a. HasCallStack => [a] -> a
head [Type]
args2)
                       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] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2
                 , let knN_cls :: Class
knN_cls = KnownNatDefs -> Class
knownBoolNat2 KnownNatDefs
defs
                       ki :: Type
ki      = (() :: Constraint) => Type -> Type
Type -> Type
typeKind ([Type] -> Type
forall a. HasCallStack => [a] -> a
head [Type]
args0)
                       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] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
                 , CommandLineOption
fn0 CommandLineOption -> CommandLineOption -> Bool
forall a. Eq a => a -> a -> Bool
== CommandLineOption
"Data.Type.Bool.If"
                 , let args0N :: [Type]
args0N = [Type] -> [Type]
forall a. HasCallStack => [a] -> [a]
tail [Type]
args0
                       args1N :: [Type]
args1N = [Type] -> Type
forall a. HasCallStack => [a] -> a
head [Type]
args0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
fn1Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type] -> [Type]
forall a. HasCallStack => [a] -> [a]
tail [Type]
args0
                       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]
args0N,[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 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)
          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))
      -- 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 (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 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 -> Maybe (Type, Type)
unEq Type
ty' = case Type -> Pred
classifyPredType Type
ty' of
                       EqPred EqRel
NomEq Type
ty1 Type
ty2 -> (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
ty1,Type
ty2)
                       Pred
_ -> Maybe (Type, Type)
forall a. Maybe a
Nothing
          rewrites :: [(Type, Type)]
rewrites = ((CType, EvExpr) -> Maybe (Type, Type))
-> [(CType, EvExpr)] -> [(Type, Type)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Type -> Maybe (Type, Type)
unEq (Type -> Maybe (Type, Type))
-> ((CType, EvExpr) -> Type)
-> (CType, EvExpr)
-> Maybe (Type, 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
          -- Rewrite
          rewriteTy :: Type -> (Type, Type) -> Maybe Type
rewriteTy Type
tyK (Type
ty1,Type
ty2) | Type
ty1 Type -> Type -> Bool
`eqType` Type
tyK = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty2
                                  | Type
ty2 Type -> Type -> Bool
`eqType` Type
tyK = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty1
                                  | Bool
otherwise        = Maybe Type
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]
knownsR  = [Maybe Type] -> [Type]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Type] -> [Type]) -> [Maybe Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Type -> [Maybe Type]) -> [Type] -> [Maybe Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Type
t -> ((Type, Type) -> Maybe Type) -> [(Type, Type)] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> (Type, Type) -> Maybe Type
rewriteTy Type
t) [(Type, Type)]
rewrites) [Type]
knowns
          knownsX :: [Type]
knownsX  = [Type]
knowns [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
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 :: [(CoreSOP, Type)]
exploded = (Type -> (CoreSOP, Type)) -> [Type] -> [(CoreSOP, Type)]
forall a b. (a -> b) -> [a] -> [b]
map ((CoreSOP, [(Type, Type)]) -> CoreSOP
forall a b. (a, b) -> a
fst ((CoreSOP, [(Type, Type)]) -> CoreSOP)
-> (Type -> (CoreSOP, [(Type, Type)])) -> Type -> 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 -> Writer [(Type, Type)] CoreSOP)
-> Type
-> (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 -> Type) -> Type -> Writer [(Type, Type)] CoreSOP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
subWant (Type -> CoreSOP) -> (Type -> Type) -> Type -> (CoreSOP, Type)
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 -> Type
forall a. a -> a
id)
                         [Type]
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, Symbol DFunId c)]
interesting = ((CoreSOP, Type) -> Maybe (Type, Symbol DFunId c))
-> [(CoreSOP, Type)] -> [(Type, Symbol DFunId c)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((CoreSOP -> Type -> Maybe (Type, Symbol DFunId c))
-> (CoreSOP, Type) -> Maybe (Type, Symbol DFunId c)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CoreSOP -> Type -> Maybe (Type, Symbol DFunId c)
forall {v} {c} {a} {c}. SOP v c -> a -> Maybe (a, Symbol v c)
examineDiff) [(CoreSOP, Type)]
exploded
      -- convert the first suitable evidence
      ((Type
h,Symbol DFunId CType
corr):[(Type, Symbol DFunId CType)]
_) <- [(Type, Symbol DFunId CType)]
-> MaybeT TcPluginM [(Type, Symbol DFunId CType)]
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Type, Symbol DFunId CType)]
forall {c}. [(Type, Symbol DFunId c)]
interesting
      Type
x <- case Symbol DFunId CType
corr of
                I Integer
0 -> Type -> MaybeT TcPluginM Type
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
h
                I Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
                    -> Type -> MaybeT TcPluginM Type
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Type
h,Integer -> Type
mkNumLitTy (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)])
                    | Bool
otherwise
                    -> Type -> MaybeT TcPluginM Type
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
h,Integer -> Type
mkNumLitTy Integer
i])
                -- 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 ->
                       Type -> MaybeT TcPluginM Type
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatDivTyCon [Type
h,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 [Integer -> Symbol DFunId CType
forall v c. Integer -> Symbol v c
I Integer
2]])])
                -- 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 -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Bool
eqType (DFunId -> Type
TyVarTy DFunId
v)) [Type]
knownsX
                    -> TcPluginM (Maybe Type) -> MaybeT TcPluginM Type
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe Type -> TcPluginM (Maybe Type)
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing)
                Symbol DFunId CType
_ -> Type -> MaybeT TcPluginM Type
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
h,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]])])
      TcPluginM (Maybe (EvTerm, [Ct])) -> MaybeT TcPluginM (EvTerm, [Ct])
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Type -> TcPluginM (Maybe (EvTerm, [Ct]))
go Type
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 EvTerm
makeOpDict :: (Class, DFunId)
-> Class -> [Type] -> [Type] -> Type -> [EvExpr] -> Maybe EvTerm
makeOpDict (Class
opCls,DFunId
dfid) Class
knCls [Type]
tyArgsC [Type]
tyArgsI Type
z [EvExpr]
evArgs
  | Just (Type
_, TcCoercion
kn_co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe (Class -> TyCon
classTyCon Class
knCls) [Type
z]
    -- 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
_, TcCoercion
kn_co_rep) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe TyCon
kn_tcRep [Type
z]
    -- SNat n ~ Integer
  , Just (Type
_, TcCoercion
op_co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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
_, TcCoercion
op_co_rep) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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 :: TcCoercion
op_to_kn  = TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
op_co_dict TcCoercion
op_co_rep)
                                (TcCoercion -> TcCoercion
mkTcSymCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
kn_co_dict TcCoercion
kn_co_rep))
        -- KnownNatAdd a b ~ KnownNat (a+b)
        ev_tm :: EvTerm
ev_tm     = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
dfun_inst TcCoercion
op_to_kn
  = 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
_, TcCoercion
kn_co_dict_z) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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
_, TcCoercion
kn_co_rep_z) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe TyCon
kn_tcRep [Type
z]
    -- SNat z ~ Integer
  , Just (Type
_, TcCoercion
kn_co_rep_x) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe TyCon
kn_tcRep [Type
x]
    -- Integer ~ SNat x
  , Just (Type
_, TcCoercion
kn_co_dict_x) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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)
-> (TcCoercion -> EvTerm) -> TcCoercion -> Maybe EvTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
xEv (TcCoercion -> Maybe EvTerm) -> TcCoercion -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ (TcCoercion
kn_co_dict_x TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
kn_co_rep_x) TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion -> TcCoercion
mkTcSymCo (TcCoercion
kn_co_dict_z TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
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
_, TcCoercion
co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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
_, TcCoercion
co_rep) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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
getPlatform
    let et :: EvExpr
et = Platform -> Integer -> EvExpr
mkNaturalExpr Platform
platform Integer
i
        ev_tm :: EvTerm
ev_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
et (TcCoercion -> TcCoercion
mkTcSymCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
co_dict TcCoercion
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
_, TcCoercion
kn_co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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 :: TcCoercion
kn_co_rep = UnivCoProvenance -> Role -> Type -> Type -> TcCoercion
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
_, TcCoercion
op_co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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
_, TcCoercion
op_co_rep) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
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 :: TcCoercion
op_to_kn  = TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
op_co_dict TcCoercion
op_co_rep)
                                (TcCoercion -> TcCoercion
mkTcSymCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
kn_co_dict TcCoercion
kn_co_rep))
        ev_tm :: EvTerm
ev_tm     = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
dfun_inst TcCoercion
op_to_kn
  = EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just EvTerm
ev_tm
  | Bool
otherwise
  = Maybe EvTerm
forall a. Maybe a
Nothing