{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- | experimental module to derive instances of the relevant classes for the
-- LTL interface. Not intended for use (yet).
module Logic.Ltl.TH (makeLtl) where

import Control.Applicative
import Control.Monad
import Control.Monad.Except (runExceptT)
import Control.Monad.Identity
import Control.Unification
import Control.Unification.IntVar (evalIntBindingT)
import Control.Unification.Ranked (UFailure (MismatchFailure, OccursFailure))
import Control.Unification.Ranked.IntVar
import Data.List
import Effect
import GHC.Generics
import Language.Haskell.TH
import Language.Haskell.TH.Datatype
import Logic.Ltl
import Logic.SingleStep

-- | There are three type classes that are relevant for the API in "Logic.Ltl":
--
-- 1. @InterpretLtl mod m op@
--
-- 2. @InterpretLtlHigherOrder mod m op@
--
-- 3. @InterpretEffectStateful (Const [Ltl mod]) m op@
--
-- For each of these classes, if you have an instance, there is a standard way
-- to define instance(s) for the class(es) further down on the list. That is,
-- in principle we could define
--
-- > instance InterpretLtl mod m op => InterpretLtlHigherOrder mod m op
--
-- and
--
-- > instance InterpretLtlHigherOrder mod m op => InterpretEffectStateful (Const [Ltl mod]) m op
--
-- However, we chose not do do this, and provide this macro instead, which
-- defines the "missing" instances on a case-by-case basis. This is because
-- sometimes you want to implement one of the classes further down the list,
-- and do so generally, so that GHC won't be able to pick a most specific
-- instance.
--
-- The macro relies on unification of instance heads: It will only generate
-- instances which are strictly more specific than any pre-existing instance in
-- current scope.
makeLtl :: Q [Dec]
makeLtl :: Q [Dec]
makeLtl = do
  ClassI Dec
_ [Dec]
firstInstances <- Name -> Q Info
reify ''InterpretMod
  ClassI Dec
_ [Dec]
higherInstances <- Name -> Q Info
reify ''InterpretLtlHigherOrder
  ClassI Dec
_ [Dec]
effectInstances <- Name -> Q Info
reify ''InterpretEffectStateful
  [Dec]
newHigherInstances <-
    [Dec] -> [Dec] -> (Cxt -> Type -> Q Dec) -> Q [Dec]
makeInstances
      [Dec]
firstInstances
      [Dec]
higherInstances
      ( \Cxt
ctx Type
firstInstanceHead ->
          case Type -> Type
dropSigT Type
firstInstanceHead of
            AppT (AppT (AppT Type
_InterpretLtl Type
modType) Type
domainType) Type
effectType ->
              Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD
                Maybe Overlap
forall a. Maybe a
Nothing
                Cxt
ctx
                (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [t|InterpretLtlHigherOrder $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
modType) $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
domainType) $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
effectType)|]
                Q ([Dec] -> Dec) -> Q [Dec] -> Q Dec
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: []) (Dec -> [Dec]) -> Q Dec -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Q Clause] -> Q Dec
forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
funD 'interpretLtlHigherOrder [[Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
clause [] (Exp -> Body
NormalB (Exp -> Body) -> Q Exp -> Q Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e|Direct . interpretLtl|]) []])
            Type
_ -> [Char] -> Q Dec
forall a. HasCallStack => [Char] -> a
error [Char]
"malformed 'InterpretLtl' instance head"
      )
  [Dec]
newEffectInstances <-
    [Dec] -> [Dec] -> (Cxt -> Type -> Q Dec) -> Q [Dec]
makeInstances
      ([Dec]
higherInstances [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
newHigherInstances)
      [Dec]
effectInstances
      ( \Cxt
ctx Type
higherInstanceHead ->
          case Type -> Type
dropSigT Type
higherInstanceHead of
            AppT (AppT (AppT Type
_InterpretLtlHigherOrder Type
modType) Type
domainType) Type
effectType ->
              Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD
                Maybe Overlap
forall a. Maybe a
Nothing
                (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (Cxt -> Cxt -> Cxt
forall a. [a] -> [a] -> [a]
++ Cxt
ctx)
                        (Cxt -> Cxt) -> Q Cxt -> Q Cxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Q Type] -> Q Cxt
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
                          [ [t|Semigroup $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
modType)|],
                            [t|MonadPlus $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
domainType)|],
                            [t|InterpretEffect $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
domainType) $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
effectType)|]
                          ]
                    )
                Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [t|InterpretEffectStateful (Const [Ltl $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
modType)]) $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
domainType) $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
effectType)|]
                Q ([Dec] -> Dec) -> Q [Dec] -> Q Dec
forall a b. Q (a -> b) -> Q a -> Q b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ( (Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: [])
                        (Dec -> [Dec]) -> Q Dec -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Q Clause] -> Q Dec
forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
funD
                          'interpretEffectStateful
                          [[Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
clause [] (Exp -> Body
NormalB (Exp -> Body) -> Q Exp -> Q Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e|interpretEffectStatefulFromLtlHigherOrder|]) []]
                    )
            Type
_ -> [Char] -> Q Dec
forall a. HasCallStack => [Char] -> a
error [Char]
"malformed 'InterpretLtlHigherOrder' instance head"
      )
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
newHigherInstances [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
newEffectInstances
  where
    makeInstances ::
      -- instances of the lower class
      [InstanceDec] ->
      -- instances of the higher class
      [InstanceDec] ->
      -- how to transform the constraints and instance head of the lower class
      -- into an instance of the higher class
      (Cxt -> Type -> Q InstanceDec) ->
      Q [InstanceDec]
    makeInstances :: [Dec] -> [Dec] -> (Cxt -> Type -> Q Dec) -> Q [Dec]
makeInstances [Dec]
lowerInstances [Dec]
higherInstances Cxt -> Type -> Q Dec
mkHigherInstance =
      (Dec -> Q (Maybe Dec)) -> [Dec] -> Q [Dec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM
        ( \case
            InstanceD Maybe Overlap
_ Cxt
ctx Type
lowerHead [Dec]
_ -> do
              Dec
candidateInstance <- Cxt -> Type -> Q Dec
mkHigherInstance Cxt
ctx Type
lowerHead
              case Dec
candidateInstance of
                InstanceD Maybe Overlap
_ Cxt
_ Type
candidateHead [Dec]
_ ->
                  if (Dec -> Bool) -> [Dec] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
                    ( \case
                        InstanceD Maybe Overlap
_ Cxt
_ Type
higherHead [Dec]
_ ->
                          Type -> Type
dropSigT Type
higherHead Type -> Type -> Bool
`subsumesType` Type -> Type
dropSigT Type
candidateHead
                        Dec
_ -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"expected list of instance declarations"
                    )
                    [Dec]
higherInstances
                    then Maybe Dec -> Q (Maybe Dec)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Dec
forall a. Maybe a
Nothing
                    else Maybe Dec -> Q (Maybe Dec)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Dec -> Q (Maybe Dec)) -> Maybe Dec -> Q (Maybe Dec)
forall a b. (a -> b) -> a -> b
$ Dec -> Maybe Dec
forall a. a -> Maybe a
Just Dec
candidateInstance
                Dec
_ -> [Char] -> Q (Maybe Dec)
forall a. HasCallStack => [Char] -> a
error [Char]
"malformed instance declaration"
            Dec
_ -> [Char] -> Q (Maybe Dec)
forall a. HasCallStack => [Char] -> a
error [Char]
"expected a list of instance declarations"
        )
        [Dec]
lowerInstances
      where
        mapMaybeM :: (Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
        mapMaybeM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
_ [] = [b] -> m [b]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        mapMaybeM a -> m (Maybe b)
f (a
x : [a]
xs) = do
          Maybe b
my <- a -> m (Maybe b)
f a
x
          case Maybe b
my of
            Maybe b
Nothing -> (a -> m (Maybe b)) -> [a] -> m [b]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs
            Just b
y -> (b
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
:) ([b] -> [b]) -> m [b] -> m [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> m (Maybe b)) -> [a] -> m [b]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs

    -- Remove all occurrences of @SigT t ...@ and replace them with just @t@.
    -- For type unification purposes, we're not interested in a kind
    -- signatures' being there or not.
    dropSigT :: Type -> Type
    dropSigT :: Type -> Type
dropSigT (ForallT [TyVarBndr Specificity]
bnd Cxt
ctx Type
t) = [TyVarBndr Specificity] -> Cxt -> Type -> Type
ForallT [TyVarBndr Specificity]
bnd Cxt
ctx (Type -> Type
dropSigT Type
t)
    dropSigT (ForallVisT [TyVarBndr ()]
bnds Type
t) = [TyVarBndr ()] -> Type -> Type
ForallVisT [TyVarBndr ()]
bnds (Type -> Type
dropSigT Type
t)
    dropSigT (AppT Type
l Type
r) = Type -> Type -> Type
AppT (Type -> Type
dropSigT Type
l) (Type -> Type
dropSigT Type
r)
    dropSigT (AppKindT Type
t Type
k) = Type -> Type -> Type
AppKindT (Type -> Type
dropSigT Type
t) Type
k
    dropSigT (SigT Type
t Type
_) = Type -> Type
dropSigT Type
t
    dropSigT (InfixT Type
l Name
n Type
r) = Type -> Name -> Type -> Type
InfixT (Type -> Type
dropSigT Type
l) Name
n (Type -> Type
dropSigT Type
r)
    dropSigT (UInfixT Type
l Name
n Type
r) = Type -> Name -> Type -> Type
UInfixT (Type -> Type
dropSigT Type
l) Name
n (Type -> Type
dropSigT Type
r)
    dropSigT (ParensT Type
t) = Type -> Type
ParensT (Type -> Type
dropSigT Type
t)
    dropSigT (ImplicitParamT [Char]
s Type
t) = [Char] -> Type -> Type
ImplicitParamT [Char]
s (Type -> Type
dropSigT Type
t)
    dropSigT Type
t = Type
t

-- * internal helpers

-- ** unifying 'Type's

data TypeFunctor t
  = AppTF t t
  | SigTF t Kind
  | VarTF Name
  | ConTF Name
  | PromotedTF Name
  | ParensTF t
  | TupleTF Int
  | ArrowTF
  | ListTF
  | PromotedTupleTF Int
  | PromotedNilTF
  | PromotedConsTF
  | StarTF
  | ConstraintTF
  | LitTF TyLit
  | WildCardTF
  | ImplicitParamTF String t
  deriving ((forall a b. (a -> b) -> TypeFunctor a -> TypeFunctor b)
-> (forall a b. a -> TypeFunctor b -> TypeFunctor a)
-> Functor TypeFunctor
forall a b. a -> TypeFunctor b -> TypeFunctor a
forall a b. (a -> b) -> TypeFunctor a -> TypeFunctor b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TypeFunctor a -> TypeFunctor b
fmap :: forall a b. (a -> b) -> TypeFunctor a -> TypeFunctor b
$c<$ :: forall a b. a -> TypeFunctor b -> TypeFunctor a
<$ :: forall a b. a -> TypeFunctor b -> TypeFunctor a
Functor, (forall m. Monoid m => TypeFunctor m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b)
-> (forall a. (a -> a -> a) -> TypeFunctor a -> a)
-> (forall a. (a -> a -> a) -> TypeFunctor a -> a)
-> (forall a. TypeFunctor a -> [a])
-> (forall a. TypeFunctor a -> Bool)
-> (forall a. TypeFunctor a -> Int)
-> (forall a. Eq a => a -> TypeFunctor a -> Bool)
-> (forall a. Ord a => TypeFunctor a -> a)
-> (forall a. Ord a => TypeFunctor a -> a)
-> (forall a. Num a => TypeFunctor a -> a)
-> (forall a. Num a => TypeFunctor a -> a)
-> Foldable TypeFunctor
forall a. Eq a => a -> TypeFunctor a -> Bool
forall a. Num a => TypeFunctor a -> a
forall a. Ord a => TypeFunctor a -> a
forall m. Monoid m => TypeFunctor m -> m
forall a. TypeFunctor a -> Bool
forall a. TypeFunctor a -> Int
forall a. TypeFunctor a -> [a]
forall a. (a -> a -> a) -> TypeFunctor a -> a
forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m
forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b
forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => TypeFunctor m -> m
fold :: forall m. Monoid m => TypeFunctor m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeFunctor a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeFunctor a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TypeFunctor a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TypeFunctor a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeFunctor a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeFunctor a -> a
foldl1 :: forall a. (a -> a -> a) -> TypeFunctor a -> a
$ctoList :: forall a. TypeFunctor a -> [a]
toList :: forall a. TypeFunctor a -> [a]
$cnull :: forall a. TypeFunctor a -> Bool
null :: forall a. TypeFunctor a -> Bool
$clength :: forall a. TypeFunctor a -> Int
length :: forall a. TypeFunctor a -> Int
$celem :: forall a. Eq a => a -> TypeFunctor a -> Bool
elem :: forall a. Eq a => a -> TypeFunctor a -> Bool
$cmaximum :: forall a. Ord a => TypeFunctor a -> a
maximum :: forall a. Ord a => TypeFunctor a -> a
$cminimum :: forall a. Ord a => TypeFunctor a -> a
minimum :: forall a. Ord a => TypeFunctor a -> a
$csum :: forall a. Num a => TypeFunctor a -> a
sum :: forall a. Num a => TypeFunctor a -> a
$cproduct :: forall a. Num a => TypeFunctor a -> a
product :: forall a. Num a => TypeFunctor a -> a
Foldable, Functor TypeFunctor
Foldable TypeFunctor
(Functor TypeFunctor, Foldable TypeFunctor) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeFunctor a -> f (TypeFunctor b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypeFunctor (f a) -> f (TypeFunctor a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypeFunctor a -> m (TypeFunctor b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TypeFunctor (m a) -> m (TypeFunctor a))
-> Traversable TypeFunctor
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
TypeFunctor (m a) -> m (TypeFunctor a)
forall (f :: * -> *) a.
Applicative f =>
TypeFunctor (f a) -> f (TypeFunctor a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeFunctor a -> m (TypeFunctor b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeFunctor a -> f (TypeFunctor b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeFunctor a -> f (TypeFunctor b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeFunctor a -> f (TypeFunctor b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeFunctor (f a) -> f (TypeFunctor a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeFunctor (f a) -> f (TypeFunctor a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeFunctor a -> m (TypeFunctor b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeFunctor a -> m (TypeFunctor b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
TypeFunctor (m a) -> m (TypeFunctor a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TypeFunctor (m a) -> m (TypeFunctor a)
Traversable, (forall a. TypeFunctor a -> Rep1 TypeFunctor a)
-> (forall a. Rep1 TypeFunctor a -> TypeFunctor a)
-> Generic1 TypeFunctor
forall a. Rep1 TypeFunctor a -> TypeFunctor a
forall a. TypeFunctor a -> Rep1 TypeFunctor a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a. TypeFunctor a -> Rep1 TypeFunctor a
from1 :: forall a. TypeFunctor a -> Rep1 TypeFunctor a
$cto1 :: forall a. Rep1 TypeFunctor a -> TypeFunctor a
to1 :: forall a. Rep1 TypeFunctor a -> TypeFunctor a
Generic1, Traversable TypeFunctor
Traversable TypeFunctor =>
(forall a.
 TypeFunctor a
 -> TypeFunctor a -> Maybe (TypeFunctor (Either a (a, a))))
-> Unifiable TypeFunctor
forall a.
TypeFunctor a
-> TypeFunctor a -> Maybe (TypeFunctor (Either a (a, a)))
forall (t :: * -> *).
Traversable t =>
(forall a. t a -> t a -> Maybe (t (Either a (a, a))))
-> Unifiable t
$czipMatch :: forall a.
TypeFunctor a
-> TypeFunctor a -> Maybe (TypeFunctor (Either a (a, a)))
zipMatch :: forall a.
TypeFunctor a
-> TypeFunctor a -> Maybe (TypeFunctor (Either a (a, a)))
Unifiable)

-- | Is the second type a substitution instance of the first one?
subsumesType :: Type -> Type -> Bool
subsumesType :: Type -> Type -> Bool
subsumesType Type
a Type
b = case Identity (Either (UFailure TypeFunctor IntVar) Bool)
-> Either (UFailure TypeFunctor IntVar) Bool
forall a. Identity a -> a
runIdentity (Identity (Either (UFailure TypeFunctor IntVar) Bool)
 -> Either (UFailure TypeFunctor IntVar) Bool)
-> (ExceptT
      (UFailure TypeFunctor IntVar)
      (IntBindingT TypeFunctor Identity)
      Bool
    -> Identity (Either (UFailure TypeFunctor IntVar) Bool))
-> ExceptT
     (UFailure TypeFunctor IntVar)
     (IntBindingT TypeFunctor Identity)
     Bool
-> Either (UFailure TypeFunctor IntVar) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntBindingT
  TypeFunctor Identity (Either (UFailure TypeFunctor IntVar) Bool)
-> Identity (Either (UFailure TypeFunctor IntVar) Bool)
forall (m :: * -> *) (t :: * -> *) a.
Monad m =>
IntBindingT t m a -> m a
evalIntBindingT (IntBindingT
   TypeFunctor Identity (Either (UFailure TypeFunctor IntVar) Bool)
 -> Identity (Either (UFailure TypeFunctor IntVar) Bool))
-> (ExceptT
      (UFailure TypeFunctor IntVar)
      (IntBindingT TypeFunctor Identity)
      Bool
    -> IntBindingT
         TypeFunctor Identity (Either (UFailure TypeFunctor IntVar) Bool))
-> ExceptT
     (UFailure TypeFunctor IntVar)
     (IntBindingT TypeFunctor Identity)
     Bool
-> Identity (Either (UFailure TypeFunctor IntVar) Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT @(UFailure TypeFunctor IntVar) (ExceptT
   (UFailure TypeFunctor IntVar)
   (IntBindingT TypeFunctor Identity)
   Bool
 -> Either (UFailure TypeFunctor IntVar) Bool)
-> ExceptT
     (UFailure TypeFunctor IntVar)
     (IntBindingT TypeFunctor Identity)
     Bool
-> Either (UFailure TypeFunctor IntVar) Bool
forall a b. (a -> b) -> a -> b
$ Type -> UTerm TypeFunctor IntVar
toUTerm Type
a UTerm TypeFunctor IntVar
-> UTerm TypeFunctor IntVar
-> ExceptT
     (UFailure TypeFunctor IntVar)
     (IntBindingT TypeFunctor Identity)
     Bool
forall (t :: * -> *) v (m :: * -> *) e (em :: (* -> *) -> * -> *).
(BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m),
 MonadError e (em m)) =>
UTerm t v -> UTerm t v -> em m Bool
`subsumes` Type -> UTerm TypeFunctor IntVar
toUTerm Type
b of
  Left (OccursFailure {}) -> Bool
False
  Left (MismatchFailure {}) -> Bool
False
  Right Bool
x -> Bool
x
  where
    toUTerm :: Type -> UTerm TypeFunctor IntVar
    toUTerm :: Type -> UTerm TypeFunctor IntVar
toUTerm (AppT Type
l Type
r) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ UTerm TypeFunctor IntVar
-> UTerm TypeFunctor IntVar
-> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. t -> t -> TypeFunctor t
AppTF (Type -> UTerm TypeFunctor IntVar
toUTerm Type
l) (Type -> UTerm TypeFunctor IntVar
toUTerm Type
r)
    toUTerm (SigT Type
t Type
k) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ UTerm TypeFunctor IntVar
-> Type -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. t -> Type -> TypeFunctor t
SigTF (Type -> UTerm TypeFunctor IntVar
toUTerm Type
t) Type
k
    toUTerm (VarT Name
n) = IntVar -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. v -> UTerm t v
UVar (IntVar -> UTerm TypeFunctor IntVar)
-> (Name -> IntVar) -> Name -> UTerm TypeFunctor IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntVar
IntVar (Int -> IntVar) -> (Name -> Int) -> Name -> IntVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Int
hashString ([Char] -> Int) -> (Name -> [Char]) -> Name -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
nameBase (Name -> UTerm TypeFunctor IntVar)
-> Name -> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ Name
n
      where
        -- See http://www.cse.yorku.ca/~oz/hash.html for an explanation of the magic numbers.
        hashString :: String -> Int
        hashString :: [Char] -> Int
hashString = (Int -> Char -> Int) -> Int -> [Char] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Int
h Char
c -> Int
33 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
h Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) Int
5381
    toUTerm (ConT Name
n) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ Name -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. Name -> TypeFunctor t
ConTF Name
n
    toUTerm (PromotedT Name
n) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ Name -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. Name -> TypeFunctor t
PromotedTF Name
n
    toUTerm (ParensT Type
t) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ UTerm TypeFunctor IntVar -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. t -> TypeFunctor t
ParensTF (UTerm TypeFunctor IntVar
 -> TypeFunctor (UTerm TypeFunctor IntVar))
-> UTerm TypeFunctor IntVar
-> TypeFunctor (UTerm TypeFunctor IntVar)
forall a b. (a -> b) -> a -> b
$ Type -> UTerm TypeFunctor IntVar
toUTerm Type
t
    toUTerm (TupleT Int
n) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ Int -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. Int -> TypeFunctor t
TupleTF Int
n
    toUTerm Type
ArrowT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
ArrowTF
    toUTerm Type
ListT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
ListTF
    toUTerm (PromotedTupleT Int
n) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ Int -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. Int -> TypeFunctor t
PromotedTupleTF Int
n
    toUTerm Type
PromotedNilT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
PromotedNilTF
    toUTerm Type
PromotedConsT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
PromotedConsTF
    toUTerm Type
StarT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
StarTF
    toUTerm Type
ConstraintT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
ConstraintTF
    toUTerm (LitT TyLit
l) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ TyLit -> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TyLit -> TypeFunctor t
LitTF TyLit
l
    toUTerm Type
WildCardT = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm TypeFunctor (UTerm TypeFunctor IntVar)
forall t. TypeFunctor t
WildCardTF
    toUTerm (ImplicitParamT [Char]
s Type
t) = TypeFunctor (UTerm TypeFunctor IntVar) -> UTerm TypeFunctor IntVar
forall (t :: * -> *) v. t (UTerm t v) -> UTerm t v
UTerm (TypeFunctor (UTerm TypeFunctor IntVar)
 -> UTerm TypeFunctor IntVar)
-> TypeFunctor (UTerm TypeFunctor IntVar)
-> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ [Char]
-> UTerm TypeFunctor IntVar
-> TypeFunctor (UTerm TypeFunctor IntVar)
forall t. [Char] -> t -> TypeFunctor t
ImplicitParamTF [Char]
s (Type -> UTerm TypeFunctor IntVar
toUTerm Type
t)
    toUTerm Type
t = [Char] -> UTerm TypeFunctor IntVar
forall a. HasCallStack => [Char] -> a
error ([Char] -> UTerm TypeFunctor IntVar)
-> [Char] -> UTerm TypeFunctor IntVar
forall a b. (a -> b) -> a -> b
$ [Char]
"unification for terms of shape " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not (yet) implemented"

-- ** finding the names of type variables in 'data' declarations

getDatatypeVars :: Name -> Q [Name]
getDatatypeVars :: Name -> Q [Name]
getDatatypeVars Name
dtName = do
  DatatypeInfo
    { datatypeInstTypes :: DatatypeInfo -> Cxt
datatypeInstTypes = Cxt
instTypes
    } <-
    Name -> Q DatatypeInfo
reifyDatatype Name
dtName
  [Name] -> Q [Name]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Q [Name]) -> [Name] -> Q [Name]
forall a b. (a -> b) -> a -> b
$
    (Type -> Name) -> Cxt -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map
      ( \case
          VarT Name
name -> Name
name
          SigT (VarT Name
name) Type
_ -> Name
name
          Type
_ -> [Char] -> Name
forall a. HasCallStack => [Char] -> a
error [Char]
"datatype declaration must only have type variables"
      )
      Cxt
instTypes

getEffectTyVars :: Name -> Q (Name, [Name])
getEffectTyVars :: Name -> Q (Name, [Name])
getEffectTyVars Name
effectName = do
  [Name]
tyVarNames <- Name -> Q [Name]
getDatatypeVars Name
effectName
  case [Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
tyVarNames of
    Name
_ : Name
nestTyVarName : [Name]
extraTyVarNames -> (Name, [Name]) -> Q (Name, [Name])
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
nestTyVarName, [Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
extraTyVarNames)
    [Name]
_ -> [Char] -> Q (Name, [Name])
forall a. HasCallStack => [Char] -> a
error [Char]
"expecting at least two type arguments in effect type"

getConTName :: Type -> Name
getConTName :: Type -> Name
getConTName (ConT Name
name) = Name
name
getConTName (AppT Type
x Type
_) = Type -> Name
getConTName Type
x
getConTName Type
_ = [Char] -> Name
forall a. HasCallStack => [Char] -> a
error [Char]
"expecting a type constructor applied to some arguments"