{-# 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 <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten
                       [Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
                        forall a. Maybe a
Nothing
#endif
                        [DType]
dxt
                        (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Empty) (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 forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'eliminate [DClause]
cls]
                         ]
  if Name
tyName forall a. Eq a => a -> a -> Bool
== ''(:~:)
    then do
      let [DType
l, DType
r] = [DType]
args
      Name
v    <- forall (m :: * -> *). Quote m => String -> m Name
newName String
"_v"
      EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
      case EqlJudge
dist of
        EqlJudge
NonEqual    -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
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       -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Equal: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
        EqlJudge
Undecidable -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " forall a. [a] -> [a] -> [a]
++
                         forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
      Just [DClause]
cls <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
      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 <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten
                       [Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
                        forall a. Maybe a
Nothing
#endif
                        [DType]
dxt
                        (DType -> DType -> DType
DAppT (Name -> DType
DConT ''Inhabited) (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 forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'trivial [DClause]
cls]
                         ]
  Bool
isNum <- Name -> [Type] -> Q Bool
isInstance ''Num [forall th ds. Desugar th ds => ds -> th
sweeten DType
tp]

  if | Bool
isNum -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE forall a b. (a -> b) -> a -> b
$ Integer -> Lit
IntegerL Integer
0 ]
     | Name
tyName forall a. Eq a => a -> a -> Bool
== ''Char  -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE forall a b. (a -> b) -> a -> b
$ Char -> Lit
CharL Char
'\NUL']
     | Name
tyName 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    -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Equal: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
          EqlJudge
Equal       -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE 'Refl ]
          EqlJudge
Undecidable -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " forall a. [a] -> [a] -> [a]
++
                           forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
        Just DClause
cls <- forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
        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 :: forall b.
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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> Q b
genPlaceHolder [DType]
tys
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DPat] -> DExp -> DClause
DClause forall a b. (a -> b) -> a -> b
$ Name -> [b] -> [DPat]
toPats Name
cName [b]
varDic) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name
cName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
ty
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
isEmpty
        then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DType -> b -> DExp
buildFactor DType
ty b
name
        else forall a. Maybe a
Nothing

buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause =
  forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Empty (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x")
    (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ (Name -> DExp
DVarE 'eliminate DExp -> DExp -> DExp
`DAppE`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DExp
DVarE) (forall a b. a -> b -> a
const 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 [] forall a b. (a -> b) -> a -> b
$ 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  =
  forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
    ''Inhabited (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ())
    (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE 'trivial)
    (\ Name
con [Maybe DExp]
args -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
con) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe DExp]
args )
    (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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
  = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [DBangType]
fs
fieldsVars (DRecC [DVarBangType]
fs)    = 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 DataFlavor
_ [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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
tvbs) [DType]
args
      ([DType]
cxt , ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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]
_) -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not supported data ty"
    DInfo
_ -> 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
    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)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
#else
  DNormalC <$>
#endif
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall a b. (a -> b) -> a -> b
$ 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 ,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) -> (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
vs forall a. [a] -> [a] -> [a]
++ [Name]
a, Name
b, [DType]
c)) 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 forall a. [a] -> [a] -> [a]
++ [DType
t2])) 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
_) = forall a. Maybe a
Nothing
splitType (DConT Name
n) = forall a. a -> Maybe a
Just ([], Name
n, [])
splitType DType
DArrowT = forall a. a -> Maybe a
Just ([], ''(->), [])
splitType (DLitT TyLit
_) = forall a. Maybe a
Nothing
splitType DType
DWildCardT = 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
_) = forall a. Maybe a
Nothing
#endif


data EqlJudge = NonEqual | Undecidable | Equal
              deriving (ReadPrec [EqlJudge]
ReadPrec EqlJudge
Int -> ReadS EqlJudge
ReadS [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 -> ShowS
[EqlJudge] -> ShowS
EqlJudge -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EqlJudge] -> ShowS
$cshowList :: [EqlJudge] -> ShowS
show :: EqlJudge -> String
$cshow :: EqlJudge -> String
showsPrec :: Int -> EqlJudge -> ShowS
$cshowsPrec :: Int -> EqlJudge -> ShowS
Show, EqlJudge -> EqlJudge -> Bool
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
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
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 = 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 <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
t0
  DType
s <- 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)
  = forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 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 forall a. Eq a => a -> a -> Bool
== Name
s    = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' (DVarT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ (DVarT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
DWildCardT DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ DType
DWildCardT = 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
  forall (m :: * -> *) a. Monad m => a -> m a
return (EqlJudge
pd forall a. Semigroup a => a -> a -> a
<> EqlJudge
bd)
compareType' DConstrainedT{} DType
_ = 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
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tTvBs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
sTvBs = do
      let dic :: Map Name DType
dic = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
sTvBs) (forall a b. (a -> b) -> [a] -> [b]
map (Name -> DType
DVarT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall flag. DTyVarBndr flag -> Name
dtvbToName) [DTyVarBndrUnit]
tTvBs)
      DType
s' <- 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'
      forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
bd
  | Bool
otherwise = 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
_   = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DAppT DType
t1 DType
t2) (DAppT DType
s1 DType
s2)
  = forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 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 forall a. Eq a => a -> a -> Bool
== Name
s    = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DConT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DType
DArrowT DType
DArrowT = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
compareType' DType
DArrowT DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
t) (DLitT TyLit
s)
  | TyLit
t forall a. Eq a => a -> a -> Bool
== TyLit
s    = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
_) DType
_ = 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
_ = 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 = forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ DType
DWildCardT = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DVarT Name
l) (DVarT Name
r)
  | Name
l forall a. Eq a => a -> a -> Bool
== Name
r = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
comparePred (DVarT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ (DVarT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DSigT DType
l DType
t) (DSigT DType
r DType
s) =
  forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t DType
s 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' <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
l2
  DType
r2' <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
r2
  forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
comparePred DType
l1 DType
r1 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
l) (DConT Name
r)
  | Name
l forall a. Eq a => a -> a -> Bool
== Name
r = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
_) DType
_ = 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
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
#else
comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable
#endif
comparePred (DForallT{}) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred DType
_ DType
_ = 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 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 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  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> DType
DVarT Name
t
  | Just (DConT Name
t) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
t
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return DType
prd
substPred Map Name DType
_ DType
t = 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 :: forall flag. 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) = forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrUnit]
vis
unTelescope (DForallInvis [DTyVarBndrSpec]
vis) = forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrSpec]
vis
#endif