{-|
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