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

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.GHC.TypeRep (
  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

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) = Bool
True
eqType'(CastTy Type
t1 Coercion
_c1) (CastTy Type
t2 Coercion
_c2) = Type -> Type -> Bool
eqType' Type
t1 Type
t2
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 Var
v1 ForAllTyFlag
_) Type
t1) (ForAllTy (Bndr Var
v2 ForAllTyFlag
_) Type
t2)
  = Type -> Type -> Bool
eqType' Type
t1 (Var -> Type -> Type -> Type
substType Var
v2 (Var -> Type
TyVarTy Var
v1) Type
t2)
eqType' (TyVarTy Var
v1) (TyVarTy Var
v2)
  = Var
v1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
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

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 Var
v)   = [Char]
"(RVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
v)  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
showTy (ForAllTy (Bndr Var
v ForAllTyFlag
_) Type
t)  = [Char]
"ForAllTy " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
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



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

substType :: TyVar -> Type -> Type -> Type
substType :: Var -> Type -> Type -> Type
substType Var
x Type
tx (TyConApp TyCon
c [Type]
ts)
  = TyCon -> [Type] -> Type
TyConApp TyCon
c (Var -> Type -> Type -> Type
substType Var
x Type
tx (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
substType Var
x Type
tx (AppTy Type
t1 Type
t2)
  = Type -> Type -> Type
AppTy (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t1) (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t2)
substType Var
x Type
tx (TyVarTy Var
y)
  | Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
y
  = Type
tx
  | Bool
otherwise
  = Var -> Type
TyVarTy Var
y
substType Var
x Type
tx (FunTy FunTyFlag
aaf Type
m Type
t1 Type
t2)
  = FunTyFlag -> Type -> Type -> Type -> Type
FunTy FunTyFlag
aaf Type
m (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t1) (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t2)
substType Var
x Type
tx f :: Type
f@(ForAllTy b :: VarBndr Var ForAllTyFlag
b@(Bndr Var
y ForAllTyFlag
_) Type
t)
  | Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Var
y
  = Type
f
  | Bool
otherwise
  = VarBndr Var ForAllTyFlag -> Type -> Type
ForAllTy VarBndr Var ForAllTyFlag
b (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t)
substType Var
x Type
tx (CastTy Type
t Coercion
c)
  = let ss :: Subst
ss = Subst -> VarSet -> Subst
extendSubstInScopeSet ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var
x] [Type
tx]) (Coercion -> VarSet
tyCoVarsOfCo Coercion
c)
     in Type -> Coercion -> Type
CastTy (Var -> Type -> Type -> Type
substType Var
x Type
tx Type
t) (HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
ss Coercion
c)
substType Var
x Type
tx (CoercionTy Coercion
c)
  = let ss :: Subst
ss = Subst -> VarSet -> Subst
extendSubstInScopeSet ([Var] -> [Type] -> Subst
HasDebugCallStack => [Var] -> [Type] -> Subst
zipTvSubst [Var
x] [Type
tx]) (Coercion -> VarSet
tyCoVarsOfCo Coercion
c)
     in Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Subst -> Coercion -> Coercion
Subst -> Coercion -> Coercion
substCo Subst
ss Coercion
c
substType Var
_ Type
_  (LitTy TyLit
l)
  = TyLit -> Type
LitTy TyLit
l