{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns                     #-}
module Proof.Propositional.TH where
import Proof.Propositional.Empty
import Proof.Propositional.Inhabited

import           Control.Arrow               (Kleisli (..), second)
import           Control.Monad               (forM, zipWithM)
import           Data.Foldable               (asum)
import           Data.Map                    (Map)
import qualified Data.Map                    as M
import           Data.Maybe                  (fromJust)
import           Data.Type.Equality          ((:~:) (..))
import           Language.Haskell.TH         (DecsQ, Lit (CharL, IntegerL),
                                              Name, Q, TypeQ, isInstance,
                                              newName, ppr)
import           Language.Haskell.TH.Desugar (DClause (..), DCon (..),
                                              DConFields (..), DCxt, DDec (..),
                                              DExp (..), DInfo (..),
                                              DLetDec (DFunD),
#if MIN_VERSION_th_desugar(1,10,0)
                                              DPat (DConP, DVarP), DPred,
#else
                                              DPat (DConPa, DVarPa), DPred(..),
#endif
#if MIN_VERSION_th_desugar(1,12,0)
  DForallTelescope(..),
#endif

                                              DTyVarBndr (..), DType (..),
                                              Overlap (Overlapping), desugar,
                                              dsReify, expandType, substTy,
                                              sweeten)
#if !MIN_VERSION_base(4,13,0)
import           Data.Semigroup              (Semigroup (..))
#endif
#if MIN_VERSION_th_desugar(1,12,0)
import Data.Functor (void)
#endif


-- | Macro to automatically derive @'Empty'@ instance for
--   concrete (variable-free) types which may contain products.
refute :: TypeQ -> DecsQ
refute :: TypeQ -> DecsQ
refute TypeQ
tps = do
  DType
tp <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Q DType
forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar (Type -> Q DType) -> TypeQ -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
  let Just ([Name]
_, Name
tyName, [DType]
args) = DType -> Maybe ([Name], Name, [DType])
splitType DType
tp
      mkInst :: [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls = [Dec] -> m [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> m [Dec]) -> [Dec] -> m [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
forall th ds. Desugar th ds => ds -> th
sweeten
                       [Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (Overlap -> Maybe Overlap
forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
                        Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
#endif
                        [DType]
dxt
                        (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Empty) ((DType -> DType -> DType) -> DType -> [DType] -> DType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) [DType]
args))
                        [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'eliminate [DClause]
cls]
                         ]
  if Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(:~:)
    then do
      let [DType
l, DType
r] = [DType]
args
      Name
v    <- String -> Q Name
newName String
"_v"
      EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
      case EqlJudge
dist of
        EqlJudge
NonEqual    -> [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ [Name] -> DExp -> DExp
DLamE [Name
v] (DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
v) []) ]
        EqlJudge
Equal       -> String -> DecsQ
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"Equal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
        EqlJudge
Undecidable -> String -> DecsQ
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
    else do
      ([DType]
dxt, [DCon]
cons) <- [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args (DInfo -> Q ([DType], [DCon]))
-> (Maybe DInfo -> DInfo) -> Maybe DInfo -> Q ([DType], [DCon])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DInfo -> DInfo
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DInfo -> Q ([DType], [DCon]))
-> Q (Maybe DInfo) -> Q ([DType], [DCon])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
      Just [DClause]
cls <- [Maybe DClause] -> Maybe [DClause]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([Maybe DClause] -> Maybe [DClause])
-> Q [Maybe DClause] -> Q (Maybe [DClause])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q (Maybe DClause)) -> [DCon] -> Q [Maybe DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> Q (Maybe DClause)
buildRefuteClause [DCon]
cons
      [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls

-- | Macro to automatically derive @'Inhabited'@ instance for
--   concrete (variable-free) types which may contain sums.
prove :: TypeQ -> DecsQ
prove :: TypeQ -> DecsQ
prove TypeQ
tps = do
  DType
tp <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Q DType
forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar (Type -> Q DType) -> TypeQ -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
  let Just ([Name]
_, Name
tyName, [DType]
args) = DType -> Maybe ([Name], Name, [DType])
splitType DType
tp
      mkInst :: [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls = [Dec] -> m [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> m [Dec]) -> [Dec] -> m [Dec]
forall a b. (a -> b) -> a -> b
$ [DDec] -> [Dec]
forall th ds. Desugar th ds => ds -> th
sweeten
                       [Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (Overlap -> Maybe Overlap
forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
                        Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
#endif
                        [DType]
dxt
                        (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Inhabited) ((DType -> DType -> DType) -> DType -> [DType] -> DType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) [DType]
args))
                        [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'trivial [DClause]
cls]
                         ]
  Bool
isNum <- Name -> [Type] -> Q Bool
isInstance ''Num [DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
tp]

  if | Bool
isNum -> [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE (Lit -> DExp) -> Lit -> DExp
forall a b. (a -> b) -> a -> b
$ Integer -> Lit
IntegerL Integer
0 ]
     | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Char  -> [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE (Lit -> DExp) -> Lit -> DExp
forall a b. (a -> b) -> a -> b
$ Char -> Lit
CharL Char
'\NUL']
     | Name
tyName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(:~:) -> do
        let [DType
l, DType
r] = [DType]
args
        EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
        case EqlJudge
dist of
          EqlJudge
NonEqual    -> String -> DecsQ
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"Equal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
          EqlJudge
Equal       -> [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE 'Refl ]
          EqlJudge
Undecidable -> String -> DecsQ
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> DecsQ) -> String -> DecsQ
forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                           Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. Ppr a => a -> Doc
ppr (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
     | Bool
otherwise -> do
        ([DType]
dxt, [DCon]
cons) <- [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args (DInfo -> Q ([DType], [DCon]))
-> (Maybe DInfo -> DInfo) -> Maybe DInfo -> Q ([DType], [DCon])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DInfo -> DInfo
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe DInfo -> Q ([DType], [DCon]))
-> Q (Maybe DInfo) -> Q ([DType], [DCon])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
        Just DClause
cls <- [Maybe DClause] -> Maybe DClause
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([Maybe DClause] -> Maybe DClause)
-> Q [Maybe DClause] -> Q (Maybe DClause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q (Maybe DClause)) -> [DCon] -> Q [Maybe DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> Q (Maybe DClause)
buildProveClause [DCon]
cons
        [DType] -> [DClause] -> DecsQ
forall (m :: * -> *). Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause
cls]

buildClause :: Name -> (DType -> Q b) -> (DType -> b -> DExp)
            -> (Name -> [Maybe DExp] -> Maybe DExp) -> (Name -> [b] -> [DPat])
            -> DCon -> Q (Maybe DClause)
buildClause :: Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause Name
clsName DType -> Q b
genPlaceHolder DType -> b -> DExp
buildFactor Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name -> [b] -> [DPat]
toPats (DCon [DTyVarBndrSpec]
_ [DType]
_ Name
cName DConFields
flds DType
_) = do
  let tys :: [DType]
tys = DConFields -> [DType]
fieldsVars DConFields
flds
  [b]
varDic <- (DType -> Q b) -> [DType] -> Q [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> Q b
genPlaceHolder [DType]
tys
  (DExp -> DClause) -> Maybe DExp -> Maybe DClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DPat] -> DExp -> DClause
DClause ([DPat] -> DExp -> DClause) -> [DPat] -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> [b] -> [DPat]
toPats Name
cName [b]
varDic) (Maybe DExp -> Maybe DClause)
-> ([Maybe DExp] -> Maybe DExp) -> [Maybe DExp] -> Maybe DClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name
cName ([Maybe DExp] -> Maybe DClause)
-> Q [Maybe DExp] -> Q (Maybe DClause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DType -> b -> Q (Maybe DExp)) -> [DType] -> [b] -> Q [Maybe DExp]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> b -> Q (Maybe DExp)
tryProc [DType]
tys [b]
varDic
  where
    tryProc :: DType -> b -> Q (Maybe DExp)
tryProc DType
ty b
name = do
      Bool
isEmpty <- Name -> [Type] -> Q Bool
isInstance Name
clsName ([Type] -> Q Bool) -> (Type -> [Type]) -> Type -> Q Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[]) (Type -> Q Bool) -> Type -> Q Bool
forall a b. (a -> b) -> a -> b
$ DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
ty
      Maybe DExp -> Q (Maybe DExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DExp -> Q (Maybe DExp)) -> Maybe DExp -> Q (Maybe DExp)
forall a b. (a -> b) -> a -> b
$ if Bool
isEmpty
        then DExp -> Maybe DExp
forall a. a -> Maybe a
Just (DExp -> Maybe DExp) -> DExp -> Maybe DExp
forall a b. (a -> b) -> a -> b
$ DType -> b -> DExp
buildFactor DType
ty b
name
        else Maybe DExp
forall a. Maybe a
Nothing

buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause =
  Name
-> (DType -> Q Name)
-> (DType -> Name -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [Name] -> [DPat])
-> DCon
-> Q (Maybe DClause)
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Empty (Q Name -> DType -> Q Name
forall a b. a -> b -> a
const (Q Name -> DType -> Q Name) -> Q Name -> DType -> Q Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
newName String
"_x")
    ((Name -> DExp) -> DType -> Name -> DExp
forall a b. a -> b -> a
const ((Name -> DExp) -> DType -> Name -> DExp)
-> (Name -> DExp) -> DType -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ (Name -> DExp
DVarE 'eliminate DExp -> DExp -> DExp
`DAppE`) (DExp -> DExp) -> (Name -> DExp) -> Name -> DExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DExp
DVarE) (([Maybe DExp] -> Maybe DExp) -> Name -> [Maybe DExp] -> Maybe DExp
forall a b. a -> b -> a
const [Maybe DExp] -> Maybe DExp
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum)
#if MIN_VERSION_th_desugar(1,13,0)
    (\Name
cName [Name]
ps -> [Name -> [DType] -> [DPat] -> DPat
DConP Name
cName [] ([DPat] -> DPat) -> [DPat] -> DPat
forall a b. (a -> b) -> a -> b
$ (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
ps])
#elif MIN_VERSION_th_desugar(1,10,0)
    (\cName ps -> [DConP cName $ map DVarP ps])
#else
    (\cName ps -> [DConPa cName $ map DVarPa ps])
#endif

buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause  =
  Name
-> (DType -> Q ())
-> (DType -> () -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [()] -> [DPat])
-> DCon
-> Q (Maybe DClause)
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Inhabited (Q () -> DType -> Q ()
forall a b. a -> b -> a
const (Q () -> DType -> Q ()) -> Q () -> DType -> Q ()
forall a b. (a -> b) -> a -> b
$ () -> Q ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    ((() -> DExp) -> DType -> () -> DExp
forall a b. a -> b -> a
const ((() -> DExp) -> DType -> () -> DExp)
-> (() -> DExp) -> DType -> () -> DExp
forall a b. (a -> b) -> a -> b
$ DExp -> () -> DExp
forall a b. a -> b -> a
const (DExp -> () -> DExp) -> DExp -> () -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE 'trivial)
    (\ Name
con [Maybe DExp]
args -> (DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
con) ([DExp] -> DExp) -> Maybe [DExp] -> Maybe DExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe DExp] -> Maybe [DExp]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe DExp]
args )
    (([()] -> [DPat]) -> Name -> [()] -> [DPat]
forall a b. a -> b -> a
const (([()] -> [DPat]) -> Name -> [()] -> [DPat])
-> ([()] -> [DPat]) -> Name -> [()] -> [DPat]
forall a b. (a -> b) -> a -> b
$ [DPat] -> [()] -> [DPat]
forall a b. a -> b -> a
const [])

fieldsVars :: DConFields -> [DType]
#if MIN_VERSION_th_desugar(1,8,0)
fieldsVars :: DConFields -> [DType]
fieldsVars (DNormalC Bool
_ [DBangType]
fs)
#else
fieldsVars (DNormalC fs)
#endif
  = (DBangType -> DType) -> [DBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map DBangType -> DType
forall a b. (a, b) -> b
snd [DBangType]
fs
fieldsVars (DRecC [DVarBangType]
fs)    = (DVarBangType -> DType) -> [DVarBangType] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_,Bang
_,DType
c) -> DType
c) [DVarBangType]
fs

resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
resolveSubsts :: [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args DInfo
info =
  case DInfo
info of
    (DTyConI (DDataD NewOrData
_ [DType]
cxt Name
_ [DTyVarBndrUnit]
tvbs
#if MIN_VERSION_th_desugar(1,9,0)
              Maybe DType
_
#endif
             [DCon]
dcons [DDerivClause]
_) Maybe [DDec]
_) -> do
      let dic :: Map Name DType
dic = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, DType)] -> Map Name DType)
-> [(Name, DType)] -> Map Name DType
forall a b. (a -> b) -> a -> b
$ [Name] -> [DType] -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
tvbs) [DType]
args
      ([DType]
cxt , ) ([DCon] -> ([DType], [DCon])) -> Q [DCon] -> Q ([DType], [DCon])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DCon -> Q DCon) -> [DCon] -> Q [DCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic) [DCon]
dcons
    -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []
    -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) ->  return []
    -- (DTyConI (DDataFamilyD _ ddec2) minst) ->  return []
    -- (DTyConI (DDataInstD _ ddec2 ddec3 ddec4 ddec5 ddec6) minst) ->  return []
    (DTyConI DDec
_ Maybe [DDec]
_) -> String -> Q ([DType], [DCon])
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not supported data ty"
    DInfo
_ -> String -> Q ([DType], [DCon])
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Please pass data-type"

type SubstDic = Map Name DType

substDCon :: SubstDic -> DCon -> Q DCon
substDCon :: Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic (DCon [DTyVarBndrSpec]
forall'd [DType]
cxt Name
conName DConFields
fields DType
mPhantom) =
  [DTyVarBndrSpec] -> [DType] -> Name -> DConFields -> DType -> DCon
DCon [DTyVarBndrSpec]
forall'd [DType]
cxt Name
conName
    (DConFields -> DType -> DCon) -> Q DConFields -> Q (DType -> DCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DConFields -> Q DConFields
substFields Map Name DType
dic DConFields
fields
#if MIN_VERSION_th_desugar(1,9,0)
    Q (DType -> DCon) -> Q DType -> Q DCon
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
mPhantom
#else
    <*> mapM (substTy dic) mPhantom
#endif

substFields :: SubstDic -> DConFields -> Q DConFields
substFields :: Map Name DType -> DConFields -> Q DConFields
substFields Map Name DType
subst
#if MIN_VERSION_th_desugar(1,8,0)
  (DNormalC Bool
fixi [DBangType]
fs)
#else
  (DNormalC fs)
#endif
  =
#if MIN_VERSION_th_desugar(1,8,0)
  Bool -> [DBangType] -> DConFields
DNormalC Bool
fixi ([DBangType] -> DConFields) -> Q [DBangType] -> Q DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
#else
  DNormalC <$>
#endif
  (DBangType -> Q DBangType) -> [DBangType] -> Q [DBangType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Kleisli Q DBangType DBangType -> DBangType -> Q DBangType
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli (Kleisli Q DBangType DBangType -> DBangType -> Q DBangType)
-> Kleisli Q DBangType DBangType -> DBangType -> Q DBangType
forall a b. (a -> b) -> a -> b
$ Kleisli Q DType DType -> Kleisli Q DBangType DBangType
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Kleisli Q DType DType -> Kleisli Q DBangType DBangType)
-> Kleisli Q DType DType -> Kleisli Q DBangType DBangType
forall a b. (a -> b) -> a -> b
$ (DType -> Q DType) -> Kleisli Q DType DType
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli ((DType -> Q DType) -> Kleisli Q DType DType)
-> (DType -> Q DType) -> Kleisli Q DType DType
forall a b. (a -> b) -> a -> b
$ Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst) [DBangType]
fs
substFields Map Name DType
subst (DRecC [DVarBangType]
fs) =
  [DVarBangType] -> DConFields
DRecC ([DVarBangType] -> DConFields) -> Q [DVarBangType] -> Q DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DVarBangType]
-> (DVarBangType -> Q DVarBangType) -> Q [DVarBangType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DVarBangType]
fs (\(Name
a,Bang
b,DType
c) -> (Name
a, Bang
b ,) (DType -> DVarBangType) -> Q DType -> Q DVarBangType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst DType
c)

splitType :: DType -> Maybe ([Name], Name, [DType])
#if MIN_VERSION_th_desugar(1,11,0)
splitType :: DType -> Maybe ([Name], Name, [DType])
splitType (DConstrainedT [DType]
_ DType
t) = DType -> Maybe ([Name], Name, [DType])
splitType DType
t
#if MIN_VERSION_th_desugar(1,12,0)
splitType (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
vs) DType
t) 
#else
splitType (DForallT _ vs t) 
#endif
#else
splitType (DForallT vs _ t) 
#endif
  = (\([Name]
a,Name
b,[DType]
c) -> ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
vs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
a, Name
b, [DType]
c)) (([Name], Name, [DType]) -> ([Name], Name, [DType]))
-> Maybe ([Name], Name, [DType]) -> Maybe ([Name], Name, [DType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, [DType])
splitType DType
t
splitType (DAppT DType
t1 DType
t2) = (\([Name]
a,Name
b,[DType]
c) -> ([Name]
a, Name
b, [DType]
c [DType] -> [DType] -> [DType]
forall a. [a] -> [a] -> [a]
++ [DType
t2])) (([Name], Name, [DType]) -> ([Name], Name, [DType]))
-> Maybe ([Name], Name, [DType]) -> Maybe ([Name], Name, [DType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, [DType])
splitType DType
t1
splitType (DSigT DType
t DType
_) = DType -> Maybe ([Name], Name, [DType])
splitType DType
t
splitType (DVarT Name
_) = Maybe ([Name], Name, [DType])
forall a. Maybe a
Nothing
splitType (DConT Name
n) = ([Name], Name, [DType]) -> Maybe ([Name], Name, [DType])
forall a. a -> Maybe a
Just ([], Name
n, [])
splitType DType
DArrowT = ([Name], Name, [DType]) -> Maybe ([Name], Name, [DType])
forall a. a -> Maybe a
Just ([], ''(->), [])
splitType (DLitT TyLit
_) = Maybe ([Name], Name, [DType])
forall a. Maybe a
Nothing
splitType DType
DWildCardT = Maybe ([Name], Name, [DType])
forall a. Maybe a
Nothing
#if !MIN_VERSION_th_desugar(1,9,0)
splitType DStarT = Nothing
#elif MIN_VERSION_th_desugar(1,10,0)
splitType (DAppKindT DType
_ DType
_) = Maybe ([Name], Name, [DType])
forall a. Maybe a
Nothing
#endif


data EqlJudge = NonEqual | Undecidable | Equal
              deriving (ReadPrec [EqlJudge]
ReadPrec EqlJudge
Int -> ReadS EqlJudge
ReadS [EqlJudge]
(Int -> ReadS EqlJudge)
-> ReadS [EqlJudge]
-> ReadPrec EqlJudge
-> ReadPrec [EqlJudge]
-> Read EqlJudge
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [EqlJudge]
$creadListPrec :: ReadPrec [EqlJudge]
readPrec :: ReadPrec EqlJudge
$creadPrec :: ReadPrec EqlJudge
readList :: ReadS [EqlJudge]
$creadList :: ReadS [EqlJudge]
readsPrec :: Int -> ReadS EqlJudge
$creadsPrec :: Int -> ReadS EqlJudge
Read, Int -> EqlJudge -> String -> String
[EqlJudge] -> String -> String
EqlJudge -> String
(Int -> EqlJudge -> String -> String)
-> (EqlJudge -> String)
-> ([EqlJudge] -> String -> String)
-> Show EqlJudge
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [EqlJudge] -> String -> String
$cshowList :: [EqlJudge] -> String -> String
show :: EqlJudge -> String
$cshow :: EqlJudge -> String
showsPrec :: Int -> EqlJudge -> String -> String
$cshowsPrec :: Int -> EqlJudge -> String -> String
Show, EqlJudge -> EqlJudge -> Bool
(EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool) -> Eq EqlJudge
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqlJudge -> EqlJudge -> Bool
$c/= :: EqlJudge -> EqlJudge -> Bool
== :: EqlJudge -> EqlJudge -> Bool
$c== :: EqlJudge -> EqlJudge -> Bool
Eq, Eq EqlJudge
Eq EqlJudge
-> (EqlJudge -> EqlJudge -> Ordering)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> Bool)
-> (EqlJudge -> EqlJudge -> EqlJudge)
-> (EqlJudge -> EqlJudge -> EqlJudge)
-> Ord EqlJudge
EqlJudge -> EqlJudge -> Bool
EqlJudge -> EqlJudge -> Ordering
EqlJudge -> EqlJudge -> EqlJudge
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EqlJudge -> EqlJudge -> EqlJudge
$cmin :: EqlJudge -> EqlJudge -> EqlJudge
max :: EqlJudge -> EqlJudge -> EqlJudge
$cmax :: EqlJudge -> EqlJudge -> EqlJudge
>= :: EqlJudge -> EqlJudge -> Bool
$c>= :: EqlJudge -> EqlJudge -> Bool
> :: EqlJudge -> EqlJudge -> Bool
$c> :: EqlJudge -> EqlJudge -> Bool
<= :: EqlJudge -> EqlJudge -> Bool
$c<= :: EqlJudge -> EqlJudge -> Bool
< :: EqlJudge -> EqlJudge -> Bool
$c< :: EqlJudge -> EqlJudge -> Bool
compare :: EqlJudge -> EqlJudge -> Ordering
$ccompare :: EqlJudge -> EqlJudge -> Ordering
$cp1Ord :: Eq EqlJudge
Ord)

instance Semigroup EqlJudge where
  EqlJudge
NonEqual    <> :: EqlJudge -> EqlJudge -> EqlJudge
<> EqlJudge
_        = EqlJudge
NonEqual
  EqlJudge
Undecidable <> EqlJudge
NonEqual = EqlJudge
NonEqual
  EqlJudge
Undecidable <> EqlJudge
_        = EqlJudge
Undecidable
  EqlJudge
Equal       <> EqlJudge
m        = EqlJudge
m

instance Monoid EqlJudge where
  mappend :: EqlJudge -> EqlJudge -> EqlJudge
mappend = EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: EqlJudge
mempty = EqlJudge
Equal

compareType :: DType -> DType -> Q EqlJudge
compareType :: DType -> DType -> Q EqlJudge
compareType DType
t0 DType
s0 = do
  DType
t <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
t0
  DType
s <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
s0
  DType -> DType -> Q EqlJudge
compareType' DType
t DType
s

compareType' :: DType -> DType -> Q EqlJudge
compareType' :: DType -> DType -> Q EqlJudge
compareType' (DSigT DType
t1 DType
t2) (DSigT DType
s1 DType
s2)
  = EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DSigT DType
t DType
_) DType
s
  = DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' DType
t (DSigT DType
s DType
_)
  = DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' (DVarT Name
t) (DVarT Name
s)
  | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s    = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' (DVarT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ (DVarT Name
_) = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
DWildCardT DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ DType
DWildCardT = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
#if MIN_VERSION_th_desugar(1,11,0)
compareType' (DConstrainedT [DType]
tCxt DType
t) (DConstrainedT [DType]
sCxt DType
s) = do
  EqlJudge
pd <- [DType] -> [DType] -> Q EqlJudge
compareCxt [DType]
tCxt [DType]
sCxt
  EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
  EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return (EqlJudge
pd EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
<> EqlJudge
bd)
compareType' DConstrainedT{} DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if MIN_VERSION_th_desugar(1,12,0)
compareType' (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
tTvBs) DType
t) (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
sTvBs) DType
s)
#else
compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)
#endif
  | [DTyVarBndrUnit] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tTvBs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [DTyVarBndrUnit] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
sTvBs = do
      let dic :: Map Name DType
dic = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, DType)] -> Map Name DType)
-> [(Name, DType)] -> Map Name DType
forall a b. (a -> b) -> a -> b
$ [Name] -> [DType] -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
sTvBs) ((DTyVarBndrUnit -> DType) -> [DTyVarBndrUnit] -> [DType]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> DType
DVarT (Name -> DType)
-> (DTyVarBndrUnit -> Name) -> DTyVarBndrUnit -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
dtvbToName) [DTyVarBndrUnit]
tTvBs)
      DType
s' <- Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
s
      EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s'
      EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
bd
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#else
compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
  | length tTvBs == length sTvBs = do
      let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
      s' <- substTy dic s
      pd <- compareCxt tCxt =<< mapM (substPred dic) sCxt
      bd <- compareType' t s'
      return (pd <> bd)
  | otherwise = return NonEqual
#endif
compareType' DForallT{} DType
_   = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DAppT DType
t1 DType
t2) (DAppT DType
s1 DType
s2)
  = EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DConT Name
t) (DConT Name
s)
  | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s    = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DConT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DType
DArrowT DType
DArrowT = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
compareType' DType
DArrowT DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
t) (DLitT TyLit
s)
  | TyLit
t TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
s    = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if !MIN_VERSION_th_desugar(1,9,0)
compareType' DStarT DStarT = return NonEqual
#endif
compareType' DType
_ DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual

compareCxt :: DCxt -> DCxt -> Q EqlJudge
compareCxt :: [DType] -> [DType] -> Q EqlJudge
compareCxt [DType]
l [DType]
r = [EqlJudge] -> EqlJudge
forall a. Monoid a => [a] -> a
mconcat ([EqlJudge] -> EqlJudge) -> Q [EqlJudge] -> Q EqlJudge
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DType -> DType -> Q EqlJudge)
-> [DType] -> [DType] -> Q [EqlJudge]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> DType -> Q EqlJudge
comparePred [DType]
l [DType]
r

comparePred :: DPred -> DPred -> Q EqlJudge
#if MIN_VERSION_th_desugar(1,10,0)
comparePred :: DType -> DType -> Q EqlJudge
comparePred DType
DWildCardT DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ DType
DWildCardT = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DVarT Name
l) (DVarT Name
r)
  | Name
l Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
r = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
comparePred (DVarT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ (DVarT Name
_) = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DSigT DType
l DType
t) (DSigT DType
r DType
s) =
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t DType
s Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DSigT DType
l DType
_) DType
r = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred DType
l (DSigT DType
r DType
_) = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DAppT DType
l1 DType
l2) (DAppT DType
r1 DType
r2) = do
  DType
l2' <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
l2
  DType
r2' <- DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
r2
  EqlJudge -> EqlJudge -> EqlJudge
forall a. Semigroup a => a -> a -> a
(<>) (EqlJudge -> EqlJudge -> EqlJudge)
-> Q EqlJudge -> Q (EqlJudge -> EqlJudge)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
comparePred DType
l1 DType
r1 Q (EqlJudge -> EqlJudge) -> Q EqlJudge -> Q EqlJudge
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
l2' DType
r2'
comparePred (DAppT DType
_ DType
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
l) (DConT Name
r)
  | Name
l Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
r = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
_) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if MIN_VERSION_th_desugar(1,12,0)
comparePred (DForallT DForallTelescope
_ DType
_) (DForallT DForallTelescope
_ DType
_) = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
#else
comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable
#endif
comparePred (DForallT{}) DType
_ = EqlJudge -> Q EqlJudge
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred DType
_ DType
_ = String -> Q EqlJudge
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Kind error: Expecting type-level predicate"
#else
comparePred DWildCardPr _ = return Undecidable
comparePred _ DWildCardPr = return Undecidable
comparePred (DVarPr l) (DVarPr r)
  | l == r = return Equal
comparePred (DVarPr _) _ = return Undecidable
comparePred _ (DVarPr _) = return Undecidable
comparePred (DSigPr l t) (DSigPr r s) =
  (<>) <$> compareType' t s <*> comparePred l r
comparePred (DSigPr l _) r = comparePred l r
comparePred l (DSigPr r _) = comparePred l r
comparePred (DAppPr l1 l2) (DAppPr r1 r2) = do
  l2' <- expandType l2
  r2' <- expandType r2
  (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'
comparePred (DAppPr _ _) _ = return NonEqual
comparePred (DConPr l) (DConPr r)
  | l == r = return Equal
  | otherwise = return NonEqual
comparePred (DConPr _) _ = return NonEqual
#if MIN_VERSION_th_desugar(1,9,0)
comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable
comparePred (DForallPr{}) _ = return NonEqual
#endif
#endif

substPred :: SubstDic -> DPred -> Q DPred
#if MIN_VERSION_th_desugar(1,10,0)
substPred :: Map Name DType -> DType -> Q DType
substPred Map Name DType
dic (DAppT DType
p1 DType
p2) = DType -> DType -> DType
DAppT (DType -> DType -> DType) -> Q DType -> Q (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p1 Q (DType -> DType) -> Q DType -> Q DType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
p2)
substPred Map Name DType
dic (DSigT DType
p DType
knd) = DType -> DType -> DType
DSigT (DType -> DType -> DType) -> Q DType -> Q (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p  Q (DType -> DType) -> Q DType -> Q DType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (DType -> Q DType
forall (q :: * -> *). DsMonad q => DType -> q DType
expandType (DType -> Q DType) -> Q DType -> Q DType
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Map Name DType -> DType -> Q DType
forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
knd)
substPred Map Name DType
dic prd :: DType
prd@(DVarT Name
p)
  | Just (DVarT Name
t) <- Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = DType -> Q DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> Q DType) -> DType -> Q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DVarT Name
t
  | Just (DConT Name
t) <- Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = DType -> Q DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> Q DType) -> DType -> Q DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
t
  | Bool
otherwise = DType -> Q DType
forall (m :: * -> *) a. Monad m => a -> m a
return DType
prd
substPred Map Name DType
_ DType
t = DType -> Q DType
forall (m :: * -> *) a. Monad m => a -> m a
return DType
t
#else
substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
substPred dic (DSigPr p knd) = DSigPr <$> substPred dic p  <*> (expandType =<< substTy dic knd)
substPred dic prd@(DVarPr p)
  | Just (DVarT t) <- M.lookup p dic = return $ DVarPr t
  | Just (DConT t) <- M.lookup p dic = return $ DConPr t
  | otherwise = return prd
substPred _ t = return t
#endif

{- FOURMOLU_DISABLE -}
#if MIN_VERSION_th_desugar(1,12,0)
dtvbToName :: DTyVarBndr flag -> Name
dtvbToName :: DTyVarBndr flag -> Name
dtvbToName (DPlainTV Name
n flag
_)    = Name
n
dtvbToName (DKindedTV Name
n flag
_ DType
_) = Name
n
#else
dtvbToName :: DTyVarBndr -> Name
dtvbToName (DPlainTV n)    = n
dtvbToName (DKindedTV n _) = n
#endif

#if MIN_VERSION_th_desugar(1,12,0)
unTelescope :: DForallTelescope -> [DTyVarBndr ()]
unTelescope :: DForallTelescope -> [DTyVarBndrUnit]
unTelescope (DForallVis [DTyVarBndrUnit]
vis) = (DTyVarBndrUnit -> DTyVarBndrUnit)
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> DTyVarBndrUnit
forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrUnit]
vis
unTelescope (DForallInvis [DTyVarBndrSpec]
vis) = (DTyVarBndrSpec -> DTyVarBndrUnit)
-> [DTyVarBndrSpec] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrSpec -> DTyVarBndrUnit
forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrSpec]
vis
#endif