{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE StandaloneDeriving        #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
{-# 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)

-- e368f3265b80aeb337fbac3f6a70ee54ab14edfd

mkTyArg :: TyVar -> TyVarBinder
mkTyArg :: TyVar -> TyVarBinder
mkTyArg TyVar
v = forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v ArgFlag
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 forall a. Eq a => a -> a -> Bool
== TyLit
l2  
eqType' (CoercionTy Coercion
c1) (CoercionTy Coercion
c2) 
  = Coercion
c1 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 forall a. Eq a => a -> a -> Bool
== Coercion
c2 
eqType' (FunTy AnonArgFlag
a1 Type
m1 Type
t11 Type
t12) (FunTy AnonArgFlag
a2 Type
m2 Type
t21 Type
t22)
  = AnonArgFlag
a1 forall a. Eq a => a -> a -> Bool
== AnonArgFlag
a2 Bool -> Bool -> Bool
&& Type
m1 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 ArgFlag
_) Type
t1) (ForAllTy (Bndr TyVar
v2 ArgFlag
_) Type
t2) 
  = Type -> Type -> Bool
eqType' Type
t1 (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 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 forall a. Eq a => a -> a -> Bool
== TyCon
c2 Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (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   " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
showPpr TyCon
c forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
", " (Type -> [Char]
showTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (AppTy Type
t1 Type
t2)   = [Char]
"(TAppTy " forall a. [a] -> [a] -> [a]
++ (Type -> [Char]
showTy Type
t1 forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t2) forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (TyVarTy TyVar
v)   = [Char]
"(RVar " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Symbolic a => a -> Symbol
symbol TyVar
v)  forall a. [a] -> [a] -> [a]
++ [Char]
")" 
showTy (ForAllTy (Bndr TyVar
v ArgFlag
_) Type
t)  = [Char]
"ForAllTy " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Symbolic a => a -> Symbol
symbol TyVar
v) forall a. [a] -> [a] -> [a]
++ [Char]
". (" forall a. [a] -> [a] -> [a]
++  Type -> [Char]
showTy Type
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (FunTy AnonArgFlag
af Type
_m1 Type
t1 Type
t2) = [Char]
"FunTy " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
showPpr AnonArgFlag
af forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ Type -> [Char]
showTy Type
t1 forall a. [a] -> [a] -> [a]
++ [Char]
". (" forall a. [a] -> [a] -> [a]
++  Type -> [Char]
showTy Type
t2 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 forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
sep' [Char]
s [[Char]]
xs 



-------------------------------------------------------------------------------
-- | GHC Type Substitutions ---------------------------------------------------
-------------------------------------------------------------------------------

class SubstTy a where
  subst :: TyVar -> Type -> a -> a
  subst TyVar
_ Type
_ = 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2) 
substType TyVar
x Type
tx (TyVarTy TyVar
y)   
  | forall a. Symbolic a => a -> Symbol
symbol TyVar
x forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol TyVar
y
  = Type
tx 
  | Bool
otherwise
  = TyVar -> Type
TyVarTy TyVar
y 
substType TyVar
x Type
tx (FunTy AnonArgFlag
aaf Type
m Type
t1 Type
t2)
  = AnonArgFlag -> Type -> Type -> Type -> Type
FunTy AnonArgFlag
aaf Type
m (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (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 ArgFlag
_) Type
t)  
  | forall a. Symbolic a => a -> Symbol
symbol TyVar
x forall a. Eq a => a -> a -> Bool
== forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = Type
f
  | Bool
otherwise 
  = TyVarBinder -> Type -> Type
ForAllTy TyVarBinder
b (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t) (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 forall a b. (a -> b) -> a -> b
$ 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) TyCon
c (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (FunCo Role
r Coercion
cN Coercion
c1 Coercion
c2)
  = Role -> Coercion -> Coercion -> Coercion -> Coercion
FunCo Role
r Coercion
cN (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2) -- TODO(adinapoli) Is this the correct substitution?
substCoercion TyVar
x Type
tx (ForAllCo TyVar
y Coercion
c1 Coercion
c2)
  | forall a. Symbolic a => a -> Symbol
symbol TyVar
x forall a. Eq a => a -> a -> Bool
== 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiom Branched
co) BranchIndex
bi (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx UnivCoProvenance
y) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (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 (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiomRule
ca)  (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)  
substCoercion TyVar
x Type
tx (NthCo Role
r BranchIndex
i Coercion
c)
  = Role -> BranchIndex -> Coercion -> Coercion
NthCo Role
r BranchIndex
i (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 (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (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 (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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role]
rs) (forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (\[TypeEqn]
eq -> forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx ([TypeEqn] -> Maybe TypeEqn
ps (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 = forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
xs