{-|
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 BangPatterns  #-}
{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE LambdaCase    #-}
{-# LANGUAGE MultiWayIf    #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns  #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# LANGUAGE Trustworthy   #-}

{-# OPTIONS_HADDOCK show-extensions #-}

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

-- base
import Control.Arrow
  ( (&&&), first )
import Data.Foldable
  ( asum )
import Data.List.NonEmpty as NE
  ( filter )
import Data.Maybe
  ( catMaybes, fromMaybe, mapMaybe )

-- transformers
import Control.Monad.Trans.Maybe
  ( MaybeT (..) )
import Control.Monad.Trans.Writer.Strict

-- ghc-typelits-natnormalise
import GHC.TypeLits.Normalise.SOP
  ( SOP (..), Product (..), Symbol (..) )
import GHC.TypeLits.Normalise.Unify
  ( CType (..),normaliseNat, reifySOP )

-- ghc-tcplugin-api
import GHC.TcPlugin.API
import GHC.TcPlugin.API.TyConSubst

-- ghc-typelits-knownnat
import GHC.TypeLits.KnownNat.Compat
  ( KnownNatDefs(..), lookupKnownNatDefs, mkNaturalExpr
  , coercionRKind, classMethodTy
  , irrelevantMult
  )

-- ghc
import GHC.Builtin.Names
  ( knownNatClassName )
#if MIN_VERSION_ghc(9,1,0)
import GHC.Builtin.Types
  ( promotedFalseDataCon, promotedTrueDataCon )
import GHC.Builtin.Types.Literals
  ( typeNatCmpTyCon )
#endif
import GHC.Builtin.Types.Literals
  ( typeNatAddTyCon, typeNatDivTyCon, typeNatSubTyCon )
import GHC.Core
  ( mkApps, mkTyApps )
import GHC.Core.Class
  ( classMethods, classTyVars )
import GHC.Core.Coercion
  ( instNewTyCon_maybe, mkNomReflCo, mkTyConAppCo )
import GHC.Core.DataCon
  ( dataConWrapId )
import GHC.Core.InstEnv
  ( instanceDFunId, lookupUniqueInstEnv )
import GHC.Core.TyCo.Rep
  ( Type(..), TyLit(..) )
import GHC.Core.TyCo.Subst
  ( substTyWithUnchecked )
import GHC.Core.Type
  ( coreView, piResultTys, splitFunTys )
import GHC.Core.Utils
  ( exprType, mkCast )
import GHC.Driver.Plugins
  ( Plugin (..), defaultPlugin, purePlugin )
import GHC.Plugins
  ( HasDebugCallStack )
import GHC.Tc.Types.Evidence
  ( evTermCoercion_maybe, evSelector )
import GHC.Types.Id
  ( idType )
import GHC.Types.Name
  ( nameModule_maybe, nameOccName )
import GHC.Types.Name.Occurrence
  ( occNameString )
import GHC.Types.Var
  ( DFunId )
import GHC.Unit.Module
  ( moduleName, moduleNameString )
import GHC.Utils.Outputable
  ( (<+>), vcat, text )

--------------------------------------------------------------------------------

-- | 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 = \ [CommandLineOption]
_ -> TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just (TcPlugin -> Maybe TcPlugin) -> TcPlugin -> Maybe TcPlugin
forall a b. (a -> b) -> a -> b
$ TcPlugin -> TcPlugin
mkTcPlugin TcPlugin
normalisePlugin
  , pluginRecompile = purePlugin
  }

normalisePlugin :: TcPlugin
normalisePlugin :: TcPlugin
normalisePlugin =
  TcPlugin { tcPluginInit :: TcPluginM 'Init KnownNatDefs
tcPluginInit  = TcPluginM 'Init 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 'Stop ()
tcPluginStop  = TcPluginM 'Stop () -> KnownNatDefs -> TcPluginM 'Stop ()
forall a b. a -> b -> a
const (() -> TcPluginM 'Stop ()
forall a. a -> TcPluginM 'Stop a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }

solveKnownNat :: KnownNatDefs -> [Ct] -> [Ct]
              -> TcPluginM Solve TcPluginSolveResult
solveKnownNat :: KnownNatDefs -> TcPluginSolver
solveKnownNat KnownNatDefs
_defs [Ct]
_givens []      = TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] [])
solveKnownNat KnownNatDefs
defs  [Ct]
givens  [Ct]
wanteds = do
  let givensTyConSubst :: TyConSubst
givensTyConSubst = [Ct] -> TyConSubst
mkTyConSubst [Ct]
givens
      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 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve 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 'Solve [Maybe ((EvTerm, Ct), [Ct])]
-> TcPluginM 'Solve ([(EvTerm, Ct)], [[Ct]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Ct, Class, Type, Orig Type)
 -> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct])))
-> [(Ct, Class, Type, Orig Type)]
-> TcPluginM 'Solve [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
-> TyConSubst
-> [(CType, EvExpr)]
-> (Ct, Class, Type, Orig Type)
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
constraintToEvTerm KnownNatDefs
defs TyConSubst
givensTyConSubst [(CType, EvExpr)]
given_map) [(Ct, Class, Type, Orig Type)]
kn_wanteds)
      TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve 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    = HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr   CtEvidence
ct_ev
                  in  (Type -> CType
CType Type
c_ty,EvExpr
ev)

-- | Try to create evidence for a wanted constraint
constraintToEvTerm
  :: KnownNatDefs
  -- ^ The "magic" KnownNatN classes
  -> TyConSubst
  -> [(CType,EvExpr)]
  -- ^ All the [G]iven constraints
  -> KnConstraint
  -> TcPluginM Solve (Maybe ((EvTerm,Ct),[Ct]))
constraintToEvTerm :: KnownNatDefs
-> TyConSubst
-> [(CType, EvExpr)]
-> (Ct, Class, Type, Orig Type)
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
constraintToEvTerm KnownNatDefs
defs TyConSubst
givensTyConSubst [(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 'Solve (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 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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])
_ -> [Coercion]
-> (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
go [] (Type
op,Maybe Coercion
forall a. Maybe a
Nothing)
    Maybe ((EvTerm, Ct), [Ct])
-> TcPluginM 'Solve (Maybe ((EvTerm, Ct), [Ct]))
forall a. a -> TcPluginM 'Solve 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 :: [Coercion] -> (Type, Maybe Coercion) -> TcPluginM Solve (Maybe (EvTerm,[Ct]))
    -- Look through type aliases
    go :: [Coercion]
-> (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
go [Coercion]
deps (Type -> Maybe Type
coreView -> Just Type
tyN, Maybe Coercion
coM) = [Coercion]
-> (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
go [Coercion]
deps (Type
tyN, Maybe Coercion
coM)
    -- Look through rewrites
    go [Coercion]
deps0 (Type
ty, Maybe Coercion
coM)
      | Just NonEmpty (TyCon, [Type], [Coercion])
tcapps <- TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo TyConSubst
givensTyConSubst Type
ty
      -- We are only interested in the splitTyConApp_upTo result that used a
      -- rewrite
      , withDeps :: [(TyCon, [Type], [Coercion])]
withDeps@((TyCon, [Type], [Coercion])
_:[(TyCon, [Type], [Coercion])]
_) <- ((TyCon, [Type], [Coercion]) -> Bool)
-> NonEmpty (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (\(TyCon
_,[Type]
_,[Coercion]
deps) -> Bool -> Bool
not ([Coercion] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Coercion]
deps)) NonEmpty (TyCon, [Type], [Coercion])
tcapps
      = do [Maybe (EvTerm, [Ct])]
results <- ((TyCon, [Type], [Coercion])
 -> TcPluginM 'Solve (Maybe (EvTerm, [Ct])))
-> [(TyCon, [Type], [Coercion])]
-> TcPluginM 'Solve [Maybe (EvTerm, [Ct])]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(TyCon
tc, [Type]
args, [Coercion]
deps1) -> [Coercion]
-> (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
go ([Coercion]
deps0 [Coercion] -> [Coercion] -> [Coercion]
forall a. Semigroup a => a -> a -> a
<> [Coercion]
deps1)
                                                         (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
args, Maybe Coercion
coM))
                               [(TyCon, [Type], [Coercion])]
withDeps
           Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe (EvTerm, [Ct])] -> Maybe (EvTerm, [Ct])
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum [Maybe (EvTerm, [Ct])]
results)
    -- See whether there is a given that matches it (after having looked through
    -- type aliases and rewrites)
    go [Coercion]
deps ([Coercion] -> Type -> Maybe EvTerm
go_other [Coercion]
deps -> Just EvTerm
ev, Maybe Coercion
_) = Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ((EvTerm, [Ct]) -> Maybe (EvTerm, [Ct])
forall a. a -> Maybe a
Just (EvTerm
ev,[]))
    -- And if there isn't, see whether we can construct it using a KnownNat<N>
    -- instance
    go [Coercion]
deps (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 'Solve InstEnvs
forall (m :: * -> *). MonadTcPlugin m => m 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 =
              if | 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 LookupInstanceErrReason (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)
  -- TODO: we should re-use the parsing functionality
  -- that is in GHC.TypeLits.NatNormalise.Compat.
#if MIN_VERSION_ghc(9,1,0)
                 | 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      = HasDebugCallStack => 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 LookupInstanceErrReason (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)
#endif
                 | [Type
arg0,Type
_] <- [Type]
args0
                 , let knN_cls :: Class
knN_cls = KnownNatDefs -> Class
knownBoolNat2 KnownNatDefs
defs
                       ki :: Type
ki      = HasDebugCallStack => 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 LookupInstanceErrReason (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:args0Rest :: [Type]
args0Rest@[Type
_,Type
_,Type
_]) <- [Type]
args0
                 , 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 LookupInstanceErrReason (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
. (HasDebugCallStack => 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 'Solve [(EvExpr, [Ct])]
-> TcPluginM 'Solve ([EvExpr], [[Ct]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Scaled Type -> TcPluginM 'Solve (EvExpr, [Ct]))
-> [Scaled Type] -> TcPluginM 'Solve [(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 'Solve (EvExpr, [Ct])
go_arg (Type -> TcPluginM 'Solve (EvExpr, [Ct]))
-> (Scaled Type -> Type)
-> Scaled Type
-> TcPluginM 'Solve (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 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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
-> [Coercion]
-> [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) [Coercion]
deps [EvExpr]
evs)
               else Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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
-> [Coercion]
-> [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) [Coercion]
deps [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 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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
<$> [Coercion] -> Type -> Maybe EvTerm
go_other [Coercion]
deps Type
ty)

    go [Coercion]
deps ((LitTy (NumTyLit Integer
i)), Maybe Coercion
_)
      -- Let GHC solve simple Literal constraints
      | LitTy TyLit
_ <- Type
op
      = Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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 'Solve (Maybe EvTerm)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class
-> Type -> [Coercion] -> Integer -> TcPluginM 'Solve (Maybe EvTerm)
makeLitDict Class
cls Type
op [Coercion]
deps Integer
i
    go [Coercion]
_ (Type, Maybe Coercion)
_ = Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve 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 Solve (EvExpr,[Ct])
    go_arg :: Type -> TcPluginM 'Solve (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 'Solve (EvExpr, [Ct])
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvExpr
ev,[])
      Maybe EvExpr
_ -> do
        (EvExpr
ev,Ct
wanted) <- Ct -> Type -> TcPluginM 'Solve (EvExpr, Ct)
makeWantedEv Ct
ct Type
ty
        (EvExpr, [Ct]) -> TcPluginM 'Solve (EvExpr, [Ct])
forall a. a -> TcPluginM 'Solve 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 :: [Coercion] -> Type -> Maybe EvTerm
    go_other :: [Coercion] -> Type -> Maybe EvTerm
go_other [Coercion]
deps 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 -> [Coercion] -> EvExpr -> Maybe EvTerm
makeKnCoercion Class
cls Type
ty Type
op [Coercion]
deps
      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 Solve (Maybe (EvTerm,[Ct]))
    offset :: Type -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
offset LitTy{} = Maybe (EvTerm, [Ct]) -> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall a. a -> TcPluginM 'Solve a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (EvTerm, [Ct])
forall a. Maybe a
Nothing
    offset Type
want = MaybeT (TcPluginM 'Solve) (EvTerm, [Ct])
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TcPluginM 'Solve) (EvTerm, [Ct])
 -> TcPluginM 'Solve (Maybe (EvTerm, [Ct])))
-> MaybeT (TcPluginM 'Solve) (EvTerm, [Ct])
-> TcPluginM 'Solve (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
mkSymCo (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, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))]
exploded = ((Type, Maybe (Type, Maybe Coercion))
 -> ((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion))))
-> [(Type, Maybe (Type, Maybe Coercion))]
-> [((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))]
forall a b. (a -> b) -> [a] -> [b]
map (((CoreSOP, [Coercion]), [(Type, Type)]) -> (CoreSOP, [Coercion])
forall a b. (a, b) -> a
fst (((CoreSOP, [Coercion]), [(Type, Type)]) -> (CoreSOP, [Coercion]))
-> ((Type, Maybe (Type, Maybe Coercion))
    -> ((CoreSOP, [Coercion]), [(Type, Type)]))
-> (Type, Maybe (Type, Maybe Coercion))
-> (CoreSOP, [Coercion])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Writer [(Type, Type)] (CoreSOP, [Coercion])
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Writer [(Type, Type)] (CoreSOP, [Coercion])
 -> ((CoreSOP, [Coercion]), [(Type, Type)]))
-> ((Type, Maybe (Type, Maybe Coercion))
    -> Writer [(Type, Type)] (CoreSOP, [Coercion]))
-> (Type, Maybe (Type, Maybe Coercion))
-> ((CoreSOP, [Coercion]), [(Type, Type)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Writer [(Type, Type)] (CoreSOP, [Coercion])
normaliseNat (Type -> Writer [(Type, Type)] (CoreSOP, [Coercion]))
-> ((Type, Maybe (Type, Maybe Coercion)) -> Type)
-> (Type, Maybe (Type, Maybe Coercion))
-> Writer [(Type, Type)] (CoreSOP, [Coercion])
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, [Coercion]))
-> ((Type, Maybe (Type, Maybe Coercion))
    -> (Type, Maybe (Type, Maybe Coercion)))
-> (Type, Maybe (Type, Maybe Coercion))
-> ((CoreSOP, [Coercion]), (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, c) -> a -> Maybe (a, Symbol v c, c)
examineDiff ((S [P [I Integer
n]]),c
deps) a
entire = (a, Symbol v c, c) -> Maybe (a, Symbol v c, c)
forall a. a -> Maybe a
Just (a
entire,Integer -> Symbol v c
forall v c. Integer -> Symbol v c
I Integer
n,c
deps)
          examineDiff ((S [P [V v
v]]),c
deps) a
entire = (a, Symbol v c, c) -> Maybe (a, Symbol v c, c)
forall a. a -> Maybe a
Just (a
entire,v -> Symbol v c
forall v c. v -> Symbol v c
V v
v,c
deps)
          examineDiff (SOP v c, c)
_ a
_ = Maybe (a, Symbol v c, c)
forall a. Maybe a
Nothing
          interesting :: [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c,
  [Coercion])]
interesting = (((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))
 -> Maybe
      ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c,
       [Coercion]))
-> [((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))]
-> [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c,
     [Coercion])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (((CoreSOP, [Coercion])
 -> (Type, Maybe (Type, Maybe Coercion))
 -> Maybe
      ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c,
       [Coercion]))
-> ((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))
-> Maybe
     ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c, [Coercion])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (CoreSOP, [Coercion])
-> (Type, Maybe (Type, Maybe Coercion))
-> Maybe
     ((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c, [Coercion])
forall {v} {c} {c} {a} {c}.
(SOP v c, c) -> a -> Maybe (a, Symbol v c, c)
examineDiff) [((CoreSOP, [Coercion]), (Type, Maybe (Type, Maybe Coercion)))]
exploded
      -- convert the first suitable evidence
      (((Type
h,Maybe (Type, Maybe Coercion)
sM),Symbol DFunId CType
corr,[Coercion]
deps):[((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType,
  [Coercion])]
_) <- [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType,
  [Coercion])]
-> MaybeT
     (TcPluginM 'Solve)
     [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType,
       [Coercion])]
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId CType,
  [Coercion])]
forall {c}.
[((Type, Maybe (Type, Maybe Coercion)), Symbol DFunId c,
  [Coercion])]
interesting
      (Type, Maybe Coercion)
x <- case Symbol DFunId CType
corr of
                I Integer
0 -> (Type, Maybe Coercion)
-> MaybeT (TcPluginM 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 (HasDebugCallStack => 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 (HasDebugCallStack => 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 (HasDebugCallStack => 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 'Solve (Maybe (Type, Maybe Coercion))
-> MaybeT (TcPluginM 'Solve) (Type, Maybe Coercion)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (Type, Maybe Coercion))
forall a. a -> TcPluginM 'Solve 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 (HasDebugCallStack => 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 'Solve) (Type, Maybe Coercion)
forall a. a -> MaybeT (TcPluginM 'Solve) 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 'Solve (Maybe (EvTerm, [Ct]))
-> MaybeT (TcPluginM 'Solve) (EvTerm, [Ct])
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT ([Coercion]
-> (Type, Maybe Coercion)
-> TcPluginM 'Solve (Maybe (EvTerm, [Ct]))
go [Coercion]
deps (Type, Maybe Coercion)
x)

makeWantedEv
  :: Ct
  -> Type
  -> TcPluginM Solve (EvExpr,Ct)
makeWantedEv :: Ct -> Type -> TcPluginM 'Solve (EvExpr, Ct)
makeWantedEv Ct
ct Type
ty = do
  -- Create a new wanted constraint
  CtEvidence
wantedCtEv <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
ty
  let ev :: EvExpr
ev      = HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
wantedCtEv
      wanted :: Ct
wanted  = CtEvidence -> Ct
mkNonCanonical CtEvidence
wantedCtEv
  (EvExpr, Ct) -> TcPluginM 'Solve (EvExpr, Ct)
forall a. a -> TcPluginM 'Solve 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
  -> [Coercion]
  -- ^ Dependent coercions
  -> [EvExpr]
  -- ^ Evidence arguments
  -> Maybe (Type, Coercion)
  -> Maybe EvTerm
makeOpDict :: (Class, DFunId)
-> Class
-> [Type]
-> [Type]
-> Type
-> [Coercion]
-> [EvExpr]
-> Maybe (Type, Coercion)
-> Maybe EvTerm
makeOpDict (Class
opCls,DFunId
dfid) Class
knCls [Type]
tyArgsC [Type]
tyArgsI Type
z [Coercion]
deps [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
    -- SNatKn (a+b) ~ Integer
  , let dfun_inst :: EvExpr
dfun_inst = DFunId -> [Type] -> [EvExpr] -> EvExpr
evDFunApp DFunId
dfid [Type]
tyArgsI [EvExpr]
evArgs
        -- KnownNatAdd a b
  , let op_to_kn :: EvExpr -> EvExpr
        op_to_kn :: EvExpr -> EvExpr
op_to_kn EvExpr
ev
            = HasDebugCallStack =>
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat Class
knCls [Type
z1] [Coercion]
deps
            (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr
Class -> [Type] -> EvExpr -> EvExpr
unwrapUnaryClassOverNewtype Class
opCls [Type]
tyArgsC EvExpr
ev
        -- KnownNatAdd a b ~ KnownNat (a+b)
  , let op_to_kn1 :: EvExpr -> EvExpr
op_to_kn1 EvExpr
ev = case Maybe (Type, Coercion)
sM of
          Maybe (Type, Coercion)
Nothing -> EvExpr -> EvExpr
op_to_kn EvExpr
ev
          Just (Type
_,Coercion
rw) ->
            let kn_co_rw :: Coercion
kn_co_rw = HasDebugCallStack => 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 = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-knownnat" Role
Representational
                              [Coercion]
deps
                              (Coercion -> Type
coercionRKind Coercion
kn_co_rw)
                              (TyCon -> [Type] -> Type
mkTyConApp (Class -> TyCon
classTyCon Class
knCls) [Type
z])
              in HasDebugCallStack => EvExpr -> Coercion -> EvExpr
EvExpr -> Coercion -> EvExpr
mkCast (EvExpr -> EvExpr
op_to_kn EvExpr
ev) (Coercion -> Coercion -> Coercion
mkTransCo Coercion
kn_co_rw Coercion
kn_co_co)
  = EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvExpr
op_to_kn1 EvExpr
dfun_inst

{-
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
               -> [Coercion]     -- ^ Dependent coercions
               -> EvExpr
               -- ^ KnownNat dictionary for the argument
               -> Maybe EvTerm
makeKnCoercion :: Class -> Type -> Type -> [Coercion] -> EvExpr -> Maybe EvTerm
makeKnCoercion Class
knCls Type
x Type
z [Coercion]
deps EvExpr
knownNat_x
  = EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack =>
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat Class
knCls [Type
z] [Coercion]
deps
                  (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr
Class -> [Type] -> EvExpr -> EvExpr
unwrapUnaryClassOverNewtype Class
knCls [Type
x] EvExpr
knownNat_x

-- | 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
            -> [Coercion]
                 -- ^ dependent coercions
            -> Integer
            -> TcPluginM Solve (Maybe EvTerm)
makeLitDict :: Class
-> Type -> [Coercion] -> Integer -> TcPluginM 'Solve (Maybe EvTerm)
makeLitDict Class
clas Type
ty [Coercion]
deps Integer
i
  = do
    EvExpr
et <- Integer -> TcPluginM 'Solve EvExpr
mkNaturalExpr Integer
i
    let
      ev_tm :: EvExpr
ev_tm = HasDebugCallStack =>
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat Class
clas [Type
ty] [Coercion]
deps EvExpr
et
    Maybe EvTerm -> TcPluginM 'Solve (Maybe EvTerm)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvTerm
EvExpr EvExpr
ev_tm)

{- |
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
  -> [Coercion]
  -- ^ Dependent coercions
  -> [EvExpr]
  -- ^ Evidence arguments
  -> Maybe EvTerm
makeOpDictByFiat :: (Class, DFunId)
-> Class
-> [Type]
-> [Type]
-> Type
-> [Coercion]
-> [EvExpr]
-> Maybe EvTerm
makeOpDictByFiat (Class
opCls,DFunId
dfid) Class
knCls [Type]
tyArgsC [Type]
tyArgsI Type
z [Coercion]
deps [EvExpr]
evArgs
  = EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack =>
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat Class
knCls [Type
z] [Coercion]
deps
                  (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr
Class -> [Type] -> EvExpr -> EvExpr
unwrapUnaryClassOverNewtype Class
opCls [Type]
tyArgsC EvExpr
ev0
  where
    ev0 :: EvExpr
ev0 = DFunId -> [Type] -> [EvExpr] -> EvExpr
evDFunApp DFunId
dfid [Type]
tyArgsI [EvExpr]
evArgs

-- | Given a class of the form @class C a b c where { meth :: ... }@ with
-- a single method, construct a dictionary of the class using an 'UnivCo'.
wrapUnaryClassByFiat :: HasDebugCallStack => Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat :: HasDebugCallStack =>
Class -> [Type] -> [Coercion] -> EvExpr -> EvExpr
wrapUnaryClassByFiat Class
cls [Type]
tys [Coercion]
deps EvExpr
et
  | Just DataCon
dc <- TyCon -> Maybe DataCon
tyConSingleDataCon_maybe (Class -> TyCon
classTyCon Class
cls)
  , [DFunId
meth] <- Class -> [DFunId]
classMethods Class
cls
  , let meth_ty :: Type
meth_ty = Type -> Type
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ DFunId -> Type
classMethodTy DFunId
meth
  = let
      by_fiat :: Coercion
by_fiat =
        CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-knownnat" Role
Representational
          [Coercion]
deps
          (HasDebugCallStack => EvExpr -> Type
EvExpr -> Type
exprType EvExpr
et)
          Type
meth_ty
    in
      DFunId -> EvExpr
forall b. DFunId -> Expr b
Var (DataCon -> DFunId
dataConWrapId DataCon
dc) EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys EvExpr -> [EvExpr] -> EvExpr
forall b. Expr b -> [Expr b] -> Expr b
`mkApps` [HasDebugCallStack => EvExpr -> Coercion -> EvExpr
EvExpr -> Coercion -> EvExpr
mkCast EvExpr
et Coercion
by_fiat]
  | Bool
otherwise
  = CommandLineOption -> SDoc -> EvExpr
forall a. HasCallStack => CommandLineOption -> SDoc -> a
pprPanic CommandLineOption
"wrapUnaryClassByFiat: class not of expected form" (SDoc -> EvExpr) -> SDoc -> EvExpr
forall a b. (a -> b) -> a -> b
$
      [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"cls:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls
           , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"tys:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
           ]

  where
    subst :: Type -> Type
subst = [DFunId] -> [Type] -> Type -> Type
substTyWithUnchecked (Class -> [DFunId]
classTyVars Class
cls) [Type]
tys

-- | Given a class of the form @class C a b c where { meth :: N x y }@
-- in which @N@ is a newtype, and a dictionary for this class, unwraps **both**
-- the class and the newtype to obtain the value inside the newtype.
unwrapUnaryClassOverNewtype :: HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr
unwrapUnaryClassOverNewtype :: HasDebugCallStack => Class -> [Type] -> EvExpr -> EvExpr
unwrapUnaryClassOverNewtype Class
cls [Type]
tys EvExpr
et
  | [DFunId
sel] <- Class -> [DFunId]
classMethods Class
cls
  , Just (TyCon
rep_tc, [Type]
rep_args) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Type
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ DFunId -> Type
classMethodTy DFunId
sel)
  , Just (Type
_, Coercion
co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
rep_tc [Type]
rep_args
  = HasDebugCallStack => EvExpr -> Coercion -> EvExpr
EvExpr -> Coercion -> EvExpr
mkCast (DFunId -> [Type] -> [EvExpr] -> EvExpr
evSelector DFunId
sel [Type]
tys [EvExpr
et]) Coercion
co
  | Bool
otherwise
  = CommandLineOption -> SDoc -> EvExpr
forall a. HasCallStack => CommandLineOption -> SDoc -> a
pprPanic CommandLineOption
"unwrapUnaryClassOverNewtype: class not of expected form" (SDoc -> EvExpr) -> SDoc -> EvExpr
forall a b. (a -> b) -> a -> b
$
      [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"cls:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls
           , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"tys:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
           ]
  where
    subst :: Type -> Type
subst = [DFunId] -> [Type] -> Type -> Type
substTyWithUnchecked (Class -> [DFunId]
classTyVars Class
cls) [Type]
tys