{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Haskell.Liquid.GHC.TypeRep (
mkTyArg,
showTy
) where
import Language.Haskell.Liquid.GHC.Misc (showPpr)
import Liquid.GHC.API as Ghc hiding (mkTyArg, showPpr, panic)
import Language.Fixpoint.Types (symbol)
mkTyArg :: TyVar -> TyVarBinder
mkTyArg :: TyVar -> TyVarBinder
mkTyArg TyVar
v = TyVar -> ForAllTyFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v ForAllTyFlag
Required
instance Eq Type where
Type
t1 == :: Type -> Type -> Bool
== Type
t2 = Type -> Type -> Bool
eqType' Type
t1 Type
t2
eqType' :: Type -> Type -> Bool
eqType' :: Type -> Type -> Bool
eqType' (LitTy TyLit
l1) (LitTy TyLit
l2)
= TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2
eqType' (CoercionTy Coercion
c1) (CoercionTy Coercion
c2)
= Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2
eqType'(CastTy Type
t1 Coercion
c1) (CastTy Type
t2 Coercion
c2)
= Type -> Type -> Bool
eqType' Type
t1 Type
t2 Bool -> Bool -> Bool
&& Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2
eqType' (FunTy FunTyFlag
a1 Type
m1 Type
t11 Type
t12) (FunTy FunTyFlag
a2 Type
m2 Type
t21 Type
t22)
= FunTyFlag
a1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
a2 Bool -> Bool -> Bool
&& Type
m1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
m2 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22
eqType' (ForAllTy (Bndr TyVar
v1 ForAllTyFlag
_) Type
t1) (ForAllTy (Bndr TyVar
v2 ForAllTyFlag
_) Type
t2)
= Type -> Type -> Bool
eqType' Type
t1 (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
v2 (TyVar -> Type
TyVarTy TyVar
v1) Type
t2)
eqType' (TyVarTy TyVar
v1) (TyVarTy TyVar
v2)
= TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2
eqType' (AppTy Type
t11 Type
t12) (AppTy Type
t21 Type
t22)
= Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22
eqType' (TyConApp TyCon
c1 [Type]
ts1) (TyConApp TyCon
c2 [Type]
ts2)
= TyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type -> Type -> Bool) -> [Type] -> [Type] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Bool
eqType' [Type]
ts1 [Type]
ts2)
eqType' Type
_ Type
_
= Bool
False
deriving instance (Eq tyvar, Eq argf) => Eq (VarBndr tyvar argf)
instance Eq Coercion where
Coercion
_ == :: Coercion -> Coercion -> Bool
== Coercion
_ = Bool
True
showTy :: Type -> String
showTy :: Type -> [Char]
showTy (TyConApp TyCon
c [Type]
ts) = [Char]
"(RApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyCon -> [Char]
forall a. Outputable a => a -> [Char]
showPpr TyCon
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
", " (Type -> [Char]
showTy (Type -> [Char]) -> [Type] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (AppTy Type
t1 Type
t2) = [Char]
"(TAppTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Type -> [Char]
showTy Type
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t2) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (TyVarTy TyVar
v) = [Char]
"(RVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (ForAllTy (Bndr TyVar
v ForAllTyFlag
_) Type
t) = [Char]
"ForAllTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (FunTy FunTyFlag
af Type
_m1 Type
t1 Type
t2) = [Char]
"FunTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FunTyFlag -> [Char]
forall a. Outputable a => a -> [Char]
showPpr FunTyFlag
af [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (CastTy Type
_ Coercion
_) = [Char]
"CastTy"
showTy (CoercionTy Coercion
_) = [Char]
"CoercionTy"
showTy (LitTy TyLit
_) = [Char]
"LitTy"
sep' :: String -> [String] -> String
sep' :: [Char] -> [[Char]] -> [Char]
sep' [Char]
_ [[Char]
x] = [Char]
x
sep' [Char]
_ [] = []
sep' [Char]
s ([Char]
x:[[Char]]
xs) = [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
s [[Char]]
xs
class SubstTy a where
subst :: TyVar -> Type -> a -> a
subst TyVar
_ Type
_ = a -> a
forall a. a -> a
id
instance SubstTy Type where
subst :: TyVar -> Type -> Type -> Type
subst = TyVar -> Type -> Type -> Type
substType
substType :: TyVar -> Type -> Type -> Type
substType :: TyVar -> Type -> Type -> Type
substType TyVar
x Type
tx (TyConApp TyCon
c [Type]
ts)
= TyCon -> [Type] -> Type
TyConApp TyCon
c (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
substType TyVar
x Type
tx (AppTy Type
t1 Type
t2)
= Type -> Type -> Type
AppTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substType TyVar
x Type
tx (TyVarTy TyVar
y)
| TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
= Type
tx
| Bool
otherwise
= TyVar -> Type
TyVarTy TyVar
y
substType TyVar
x Type
tx (FunTy FunTyFlag
aaf Type
m Type
t1 Type
t2)
= FunTyFlag -> Type -> Type -> Type -> Type
FunTy FunTyFlag
aaf Type
m (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substType TyVar
x Type
tx f :: Type
f@(ForAllTy b :: TyVarBinder
b@(Bndr TyVar
y ForAllTyFlag
_) Type
t)
| TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
= Type
f
| Bool
otherwise
= TyVarBinder -> Type -> Type
ForAllTy TyVarBinder
b (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t)
substType TyVar
x Type
tx (CastTy Type
t Coercion
c)
= Type -> Coercion -> Type
CastTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substType TyVar
x Type
tx (CoercionTy Coercion
c)
= Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c
substType TyVar
_ Type
_ (LitTy TyLit
l)
= TyLit -> Type
LitTy TyLit
l
instance SubstTy Coercion where
subst :: TyVar -> Type -> Coercion -> Coercion
subst = TyVar -> Type -> Coercion -> Coercion
substCoercion
substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion TyVar
x Type
tx (TyConAppCo Role
r TyCon
c [Coercion]
cs)
= Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) TyCon
c (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)
substCoercion TyVar
x Type
tx (AppCo Coercion
c1 Coercion
c2)
= Coercion -> Coercion -> Coercion
AppCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
cN Coercion
c1 Coercion
c2)
= Role
-> FunTyFlag
-> FunTyFlag
-> Coercion
-> Coercion
-> Coercion
-> Coercion
FunCo Role
r FunTyFlag
afl FunTyFlag
afr Coercion
cN (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (ForAllCo TyVar
y Coercion
c1 Coercion
c2)
| TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
= TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y Coercion
c1 Coercion
c2
| Bool
otherwise
= TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
_ Type
_ (CoVarCo TyVar
y)
= TyVar -> Coercion
CoVarCo TyVar
y
substCoercion TyVar
x Type
tx (AxiomInstCo CoAxiom Branched
co BranchIndex
bi [Coercion]
cs)
= CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
AxiomInstCo (TyVar -> Type -> CoAxiom Branched -> CoAxiom Branched
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiom Branched
co) BranchIndex
bi (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)
substCoercion TyVar
x Type
tx (UnivCo UnivCoProvenance
y Role
r Type
t1 Type
t2)
= UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo (TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx UnivCoProvenance
y) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substCoercion TyVar
x Type
tx (SymCo Coercion
c)
= Coercion -> Coercion
SymCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (TransCo Coercion
c1 Coercion
c2)
= Coercion -> Coercion -> Coercion
TransCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (AxiomRuleCo CoAxiomRule
ca [Coercion]
cs)
= CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo (TyVar -> Type -> CoAxiomRule -> CoAxiomRule
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiomRule
ca) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)
substCoercion TyVar
x Type
tx (SelCo CoSel
i Coercion
c)
= CoSel -> Coercion -> Coercion
SelCo CoSel
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (LRCo LeftOrRight
i Coercion
c)
= LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (InstCo Coercion
c1 Coercion
c2)
= Coercion -> Coercion -> Coercion
InstCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (KindCo Coercion
c)
= Coercion -> Coercion
KindCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (SubCo Coercion
c)
= Coercion -> Coercion
SubCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
_x Type
_tx (Refl Type
t)
= Type -> Coercion
Refl Type
t
substCoercion TyVar
_x Type
_tx (GRefl Role
r Type
t MCoercionN
c)
= Role -> Type -> MCoercionN -> Coercion
GRefl Role
r Type
t MCoercionN
c
substCoercion TyVar
_x Type
_tx (HoleCo CoercionHole
c)
= CoercionHole -> Coercion
HoleCo CoercionHole
c
instance SubstTy Role where
instance SubstTy (CoAxiom Branched) where
instance SubstTy UnivCoProvenance where
subst :: TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
subst TyVar
x Type
tx (PhantomProv Coercion
c)
= Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c
subst TyVar
x Type
tx (ProofIrrelProv Coercion
c)
= Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c
subst TyVar
_ Type
_ UnivCoProvenance
ch
= UnivCoProvenance
ch
instance SubstTy CoAxiomRule where
subst :: TyVar -> Type -> CoAxiomRule -> CoAxiomRule
subst TyVar
x Type
tx (CoAxiomRule FastString
n [Role]
rs Role
r [TypeEqn] -> Maybe TypeEqn
ps)
= FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule FastString
n (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Role -> Role) -> [Role] -> [Role]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role]
rs) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (\[TypeEqn]
eq -> TyVar -> Type -> Maybe TypeEqn -> Maybe TypeEqn
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx ([TypeEqn] -> Maybe TypeEqn
ps (TyVar -> Type -> [TypeEqn] -> [TypeEqn]
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx [TypeEqn]
eq)))
instance (SubstTy a, Functor m) => SubstTy (m a) where
subst :: TyVar -> Type -> m a -> m a
subst TyVar
x Type
tx m a
xs = TyVar -> Type -> a -> a
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
xs