{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE ViewPatterns              #-}

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

-- | Refinement Types. Mostly mirroring the GHC Type definition, but with
--   room for refinements of various sorts.
-- TODO: Desperately needs re-organization.

module Language.Haskell.Liquid.Types.RefType (

    TyConMap

  -- * Functions for lifting Reft-values to Spec-values
  , uTop, uReft, uRType, uRType', uRTypeGen, uPVar

  -- * Applying a solution to a SpecType
  , applySolution

  -- * Functions for decreasing arguments
  , isDecreasing, makeDecrType, makeNumEnv
  , makeLexRefa

  -- * Functions for manipulating `Predicate`s
  , pdVar
  , findPVar
  , FreeVar, allTyVars, allTyVars', freeTyVars, tyClasses, tyConName

  -- * Quantifying RTypes
  , quantifyRTy
  , quantifyFreeRTy

  -- * RType constructors
  , ofType, toType, bareOfType
  , bTyVar, rTyVar, rVar, rApp, gApp, rEx
  , symbolRTyVar, bareRTyVar
  , tyConBTyCon
  , pdVarReft

  -- * Substitutions
  , subts, subvPredicate, subvUReft
  , subsTyVarMeet, subsTyVarMeet', subsTyVarNoMeet
  , subsTyVarsNoMeet, subsTyVarsMeet

  -- * Destructors
  , addTyConInfo
  , appRTyCon
  , typeUniqueSymbol
  , classBinds
  , isSizeable
  , famInstTyConType
  , famInstArgs

  -- * Manipulating Refinements in RTypes
  , strengthen
  , generalize
  , normalizePds
  , dataConMsReft
  , dataConReft
  , rTypeSortedReft
  , rTypeSort
  , typeSort
  , shiftVV

  -- * TODO: classify these
  -- , mkDataConIdsTy
  , expandProductType
  , mkTyConInfo
  , strengthenRefTypeGen
  , strengthenDataConType
  , isBaseTy
  , updateRTVar, isValKind, kindToRType
  , rTVarInfo

  , tyVarsPosition, Positions(..)

  , isNumeric

  ) where

-- import           GHC.Stack
import Prelude hiding (error)
-- import qualified Prelude
import           Data.Maybe               (fromMaybe, isJust)
import           Data.Monoid              (First(..))
import           Data.Hashable
import qualified Data.HashMap.Strict  as M
import qualified Data.HashSet         as S
import qualified Data.List as L
import           Control.Monad  (void)
import           Text.Printf
import           Text.PrettyPrint.HughesPJ hiding ((<>), first)
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types hiding (DataDecl (..), DataCtor (..), panic, shiftVV, Predicate, isNumeric)
import           Language.Fixpoint.Types.Visitor (mapKVars, Visitable)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.PrettyPrint

import           Language.Haskell.Liquid.Types.Types hiding (R, DataConP (..))
import           Language.Haskell.Liquid.Types.Variance
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import           Language.Haskell.Liquid.GHC.Play (mapType, stringClassArg, isRecursivenewTyCon)
import           Liquid.GHC.API        as Ghc hiding ( Expr
                                                                      , Located
                                                                      , tyConName
                                                                      , punctuate
                                                                      , hcat
                                                                      , (<+>)
                                                                      , parens
                                                                      , empty
                                                                      , dcolon
                                                                      , vcat
                                                                      , nest
                                                                      , ($+$)
                                                                      , panic
                                                                      , text
                                                                      )
import           Language.Haskell.Liquid.GHC.TypeRep () -- Eq Type instance
import Data.List (foldl')







strengthenDataConType :: (Var, SpecType) -> (Var, SpecType)
strengthenDataConType :: (TyVar, SpecType) -> (TyVar, SpecType)
strengthenDataConType (TyVar
x, SpecType
t) = (TyVar
x, forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep RTypeRep RTyCon RTyVar (UReft Reft)
trep {ty_res :: SpecType
ty_res = SpecType
tres})
  where
    tres :: SpecType
tres     = forall a. PPrint a => String -> a -> a
F.notracepp String
_msg forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar (UReft Reft)
trep forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> Predicate -> UReft r
MkUReft (forall a. Expression a => a -> Reft
exprReft Expr
expr') forall a. Monoid a => a
mempty
    trep :: RTypeRep RTyCon RTyVar (UReft Reft)
trep     = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t
    _msg :: String
_msg     = String
"STRENGTHEN-DATACONTYPE x = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (TyVar
x, forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts)
    ([Symbol]
xs, [SpecType]
ts) = RTypeRep RTyCon RTyVar (UReft Reft) -> ([Symbol], [SpecType])
dataConArgs RTypeRep RTyCon RTyVar (UReft Reft)
trep
    as :: [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as       = forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars  RTypeRep RTyCon RTyVar (UReft Reft)
trep
    x' :: Symbol
x'       = forall a. Symbolic a => a -> Symbol
symbol TyVar
x
    expr' :: Expr
expr' | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol]
xs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as = Symbol -> Expr
EVar Symbol
x'
          | Bool
otherwise          = LocSymbol -> [Expr] -> Expr
mkEApp (forall a. a -> Located a
dummyLoc Symbol
x') (Symbol -> Expr
EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)


dataConArgs :: SpecRep -> ([Symbol], [SpecType])
dataConArgs :: RTypeRep RTyCon RTyVar (UReft Reft) -> ([Symbol], [SpecType])
dataConArgs RTypeRep RTyCon RTyVar (UReft Reft)
trep = forall a b. [(a, b)] -> ([a], [b])
unzip [ (Symbol
x, SpecType
t) | (Symbol
x, SpecType
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts, forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> Bool
isValTy SpecType
t]
  where
    xs :: [Symbol]
xs           = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar (UReft Reft)
trep
    ts :: [SpecType]
ts           = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar (UReft Reft)
trep
    isValTy :: RRType r -> Bool
isValTy      = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
Ghc.isEvVarType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False


pdVar :: PVar t -> Predicate
pdVar :: forall t. PVar t -> Predicate
pdVar PVar t
v        = [UsedPVar] -> Predicate
Pr [forall t. PVar t -> UsedPVar
uPVar PVar t
v]

findPVar :: [PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
findPVar :: forall c tv.
[PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
findPVar [PVar (RType c tv ())]
ps UsedPVar
upv = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
name PVKind (RType c tv ())
ty Symbol
v (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(()
_, Symbol
_, Expr
e) (RType c tv ()
t, Symbol
s, Expr
_) -> (RType c tv ()
t, Symbol
s, Expr
e)) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
upv) [(RType c tv (), Symbol, Expr)]
args)
  where
    PV Symbol
name PVKind (RType c tv ())
ty Symbol
v [(RType c tv (), Symbol, Expr)]
args = forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. PPrint a => a -> a
msg UsedPVar
upv) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((forall a. Eq a => a -> a -> Bool
== forall t. PVar t -> Symbol
pname UsedPVar
upv) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PVar t -> Symbol
pname) [PVar (RType c tv ())]
ps
    msg :: a -> a
msg a
p = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"RefType.findPVar" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp a
p forall a. [a] -> [a] -> [a]
++ String
"not found"

-- | Various functions for converting vanilla `Reft` to `Spec`

uRType          ::  RType c tv a -> RType c tv (UReft a)
uRType :: forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType          = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. r -> UReft r
uTop

uRType'         ::  RType c tv (UReft a) -> RType c tv a
uRType' :: forall c tv a. RType c tv (UReft a) -> RType c tv a
uRType'         = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. UReft r -> r
ur_reft

uRTypeGen       :: Reftable b => RType c tv a -> RType c tv b
uRTypeGen :: forall b c tv a. Reftable b => RType c tv a -> RType c tv b
uRTypeGen       = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Monoid a => a
mempty

uPVar           :: PVar t -> UsedPVar
uPVar :: forall t. PVar t -> UsedPVar
uPVar           = forall (f :: * -> *) a. Functor f => f a -> f ()
void

uReft           :: (Symbol, Expr) -> UReft Reft
uReft :: (Symbol, Expr) -> UReft Reft
uReft           = forall r. r -> UReft r
uTop forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Expr) -> Reft
Reft

uTop            ::  r -> UReft r
uTop :: forall r. r -> UReft r
uTop r
r          = forall r. r -> Predicate -> UReft r
MkUReft r
r forall a. Monoid a => a
mempty

--------------------------------------------------------------------
-------------- (Class) Predicates for Valid Refinement Types -------
--------------------------------------------------------------------


-- Monoid Instances ---------------------------------------------------------

instance ( SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) c
         , OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) tv
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         )
        => Semigroup (RType c tv r)  where
  <> :: RType c tv r -> RType c tv r -> RType c tv r
(<>) = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType

-- TODO: remove, use only Semigroup?
instance ( SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) c
         , OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) tv
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         )
        => Monoid (RType c tv r)  where
  mempty :: RType c tv r
mempty  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"mempty: RType"

-- MOVE TO TYPES
instance ( SubsTy tv (RType c tv ()) c
         , OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) tv
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         )
         => Semigroup (RTProp c tv r) where
  <> :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r
(<>) (RProp [(Symbol, RType c tv ())]
s1 (RHole r
r1)) (RProp [(Symbol, RType c tv ())]
s2 (RHole r
r2))
    | forall r. Reftable r => r -> Bool
isTauto r
r1 = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s2 (forall c tv r. r -> RType c tv r
RHole r
r2)
    | forall r. Reftable r => r -> Bool
isTauto r
r2 = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s1 (forall c tv r. r -> RType c tv r
RHole r
r1)
    | Bool
otherwise  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s1 forall a b. (a -> b) -> a -> b
$ forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ r
r1 forall r. Reftable r => r -> r -> r
`meet`
                               forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
s2) (Symbol -> Expr
EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
s1)) r
r2

  (<>) (RProp [(Symbol, RType c tv ())]
s1 RType c tv r
t1) (RProp [(Symbol, RType c tv ())]
s2 RType c tv r
t2)
    | forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType c tv r
t1 = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s2 RType c tv r
t2
    | forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType c tv r
t2 = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s1 RType c tv r
t1
    | Bool
otherwise    = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
s1 forall a b. (a -> b) -> a -> b
$ RType c tv r
t1  forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
`strengthenRefType`
                                forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
s2) (Symbol -> Expr
EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
s1)) RType c tv r
t2

-- TODO: remove and use only Semigroup?
instance ( SubsTy tv (RType c tv ()) c
         , OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) tv
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         )
         => Monoid (RTProp c tv r) where
  mempty :: RTProp c tv r
mempty  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"mempty: RTProp"
  mappend :: RTProp c tv r -> RTProp c tv r -> RTProp c tv r
mappend = forall a. Semigroup a => a -> a -> a
(<>)

{-
NV: The following makes ghc diverge thus dublicating the code
instance ( OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) c
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         , SubsTy tv (RType c tv ()) tv
         ) => Reftable (RTProp c tv r) where
  isTauto (RProp _ (RHole r)) = isTauto r
  isTauto (RProp _ t)         = isTrivial t
  top (RProp _ (RHole _))     = panic Nothing "RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp xs t)            = RProp xs $ mapReft top t
  ppTy (RProp _ (RHole r)) d  = ppTy r d
  ppTy (RProp _ _) _          = panic Nothing "RefType: Reftable ppTy in RProp"
  toReft                      = panic Nothing "RefType: Reftable toReft"
  params                      = panic Nothing "RefType: Reftable params for Ref"
  bot                         = panic Nothing "RefType: Reftable bot    for Ref"
  ofReft                      = panic Nothing "RefType: Reftable ofReft for Ref"
-}

instance Reftable (RTProp RTyCon RTyVar (UReft Reft)) where
  isTauto :: RTProp RTyCon RTyVar (UReft Reft) -> Bool
isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole UReft Reft
r)) = forall r. Reftable r => r -> Bool
isTauto UReft Reft
r
  isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ SpecType
t)         = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial SpecType
t
  top :: RTProp RTyCon RTyVar (UReft Reft)
-> RTProp RTyCon RTyVar (UReft Reft)
top (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole UReft Reft
_))     = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp [(Symbol, RType RTyCon RTyVar ())]
xs SpecType
t)            = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs forall a b. (a -> b) -> a -> b
$ forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top SpecType
t
  ppTy :: RTProp RTyCon RTyVar (UReft Reft) -> Doc -> Doc
ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole UReft Reft
r)) Doc
d  = forall r. Reftable r => r -> Doc -> Doc
ppTy UReft Reft
r Doc
d
  ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ SpecType
_) Doc
_          = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ppTy in RProp"
  toReft :: RTProp RTyCon RTyVar (UReft Reft) -> Reft
toReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable toReft"
  params :: RTProp RTyCon RTyVar (UReft Reft) -> [Symbol]
params                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable params for Ref"
  bot :: RTProp RTyCon RTyVar (UReft Reft)
-> RTProp RTyCon RTyVar (UReft Reft)
bot                         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable bot    for Ref"
  ofReft :: Reft -> RTProp RTyCon RTyVar (UReft Reft)
ofReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ofReft for Ref"

instance Reftable (RTProp RTyCon RTyVar ()) where
  isTauto :: RTProp RTyCon RTyVar () -> Bool
isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole ()
r)) = forall r. Reftable r => r -> Bool
isTauto ()
r
  isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ RType RTyCon RTyVar ()
t)         = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType RTyCon RTyVar ()
t
  top :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar ()
top (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole ()
_))     = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp [(Symbol, RType RTyCon RTyVar ())]
xs RType RTyCon RTyVar ()
t)            = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs forall a b. (a -> b) -> a -> b
$ forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top RType RTyCon RTyVar ()
t
  ppTy :: RTProp RTyCon RTyVar () -> Doc -> Doc
ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole ()
r)) Doc
d  = forall r. Reftable r => r -> Doc -> Doc
ppTy ()
r Doc
d
  ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ RType RTyCon RTyVar ()
_) Doc
_          = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ppTy in RProp"
  toReft :: RTProp RTyCon RTyVar () -> Reft
toReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable toReft"
  params :: RTProp RTyCon RTyVar () -> [Symbol]
params                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable params for Ref"
  bot :: RTProp RTyCon RTyVar () -> RTProp RTyCon RTyVar ()
bot                         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable bot    for Ref"
  ofReft :: Reft -> RTProp RTyCon RTyVar ()
ofReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ofReft for Ref"

instance Reftable (RTProp BTyCon BTyVar (UReft Reft)) where
  isTauto :: RTProp BTyCon BTyVar (UReft Reft) -> Bool
isTauto (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole UReft Reft
r)) = forall r. Reftable r => r -> Bool
isTauto UReft Reft
r
  isTauto (RProp [(Symbol, RType BTyCon BTyVar ())]
_ RType BTyCon BTyVar (UReft Reft)
t)         = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType BTyCon BTyVar (UReft Reft)
t
  top :: RTProp BTyCon BTyVar (UReft Reft)
-> RTProp BTyCon BTyVar (UReft Reft)
top (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole UReft Reft
_))     = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp [(Symbol, RType BTyCon BTyVar ())]
xs RType BTyCon BTyVar (UReft Reft)
t)            = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType BTyCon BTyVar ())]
xs forall a b. (a -> b) -> a -> b
$ forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top RType BTyCon BTyVar (UReft Reft)
t
  ppTy :: RTProp BTyCon BTyVar (UReft Reft) -> Doc -> Doc
ppTy (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole UReft Reft
r)) Doc
d  = forall r. Reftable r => r -> Doc -> Doc
ppTy UReft Reft
r Doc
d
  ppTy (RProp [(Symbol, RType BTyCon BTyVar ())]
_ RType BTyCon BTyVar (UReft Reft)
_) Doc
_          = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ppTy in RProp"
  toReft :: RTProp BTyCon BTyVar (UReft Reft) -> Reft
toReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable toReft"
  params :: RTProp BTyCon BTyVar (UReft Reft) -> [Symbol]
params                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable params for Ref"
  bot :: RTProp BTyCon BTyVar (UReft Reft)
-> RTProp BTyCon BTyVar (UReft Reft)
bot                         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable bot    for Ref"
  ofReft :: Reft -> RTProp BTyCon BTyVar (UReft Reft)
ofReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ofReft for Ref"

instance Reftable (RTProp BTyCon BTyVar ())  where
  isTauto :: RTProp BTyCon BTyVar () -> Bool
isTauto (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole ()
r)) = forall r. Reftable r => r -> Bool
isTauto ()
r
  isTauto (RProp [(Symbol, RType BTyCon BTyVar ())]
_ RType BTyCon BTyVar ()
t)         = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType BTyCon BTyVar ()
t
  top :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar ()
top (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole ()
_))     = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp [(Symbol, RType BTyCon BTyVar ())]
xs RType BTyCon BTyVar ()
t)            = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType BTyCon BTyVar ())]
xs forall a b. (a -> b) -> a -> b
$ forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top RType BTyCon BTyVar ()
t
  ppTy :: RTProp BTyCon BTyVar () -> Doc -> Doc
ppTy (RProp [(Symbol, RType BTyCon BTyVar ())]
_ (RHole ()
r)) Doc
d  = forall r. Reftable r => r -> Doc -> Doc
ppTy ()
r Doc
d
  ppTy (RProp [(Symbol, RType BTyCon BTyVar ())]
_ RType BTyCon BTyVar ()
_) Doc
_          = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ppTy in RProp"
  toReft :: RTProp BTyCon BTyVar () -> Reft
toReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable toReft"
  params :: RTProp BTyCon BTyVar () -> [Symbol]
params                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable params for Ref"
  bot :: RTProp BTyCon BTyVar () -> RTProp BTyCon BTyVar ()
bot                         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable bot    for Ref"
  ofReft :: Reft -> RTProp BTyCon BTyVar ()
ofReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ofReft for Ref"

instance Reftable (RTProp RTyCon RTyVar Reft) where
  isTauto :: RRProp Reft -> Bool
isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole Reft
r)) = forall r. Reftable r => r -> Bool
isTauto Reft
r
  isTauto (RProp [(Symbol, RType RTyCon RTyVar ())]
_ RType RTyCon RTyVar Reft
t)         = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial RType RTyCon RTyVar Reft
t
  top :: RRProp Reft -> RRProp Reft
top (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole Reft
_))     = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable top called on (RProp _ (RHole _))"
  top (RProp [(Symbol, RType RTyCon RTyVar ())]
xs RType RTyCon RTyVar Reft
t)            = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
xs forall a b. (a -> b) -> a -> b
$ forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top RType RTyCon RTyVar Reft
t
  ppTy :: RRProp Reft -> Doc -> Doc
ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole Reft
r)) Doc
d  = forall r. Reftable r => r -> Doc -> Doc
ppTy Reft
r Doc
d
  ppTy (RProp [(Symbol, RType RTyCon RTyVar ())]
_ RType RTyCon RTyVar Reft
_) Doc
_          = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ppTy in RProp"
  toReft :: RRProp Reft -> Reft
toReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable toReft"
  params :: RRProp Reft -> [Symbol]
params                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable params for Ref"
  bot :: RRProp Reft -> RRProp Reft
bot                         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable bot    for Ref"
  ofReft :: Reft -> RRProp Reft
ofReft                      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType: Reftable ofReft for Ref"

----------------------------------------------------------------------------
-- | Subable Instances -----------------------------------------------------
----------------------------------------------------------------------------

instance Subable (RRProp Reft) where
  syms :: RRProp Reft -> [Symbol]
syms (RProp [(Symbol, RType RTyCon RTyVar ())]
ss (RHole Reft
r)) = (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> [Symbol]
syms Reft
r
  syms (RProp [(Symbol, RType RTyCon RTyVar ())]
ss RType RTyCon RTyVar Reft
t)      = (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> [Symbol]
syms RType RTyCon RTyVar Reft
t


  subst :: Subst -> RRProp Reft -> RRProp Reft
subst Subst
su (RProp [(Symbol, RType RTyCon RTyVar ())]
ss (RHole Reft
r)) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => Subst -> a -> a
subst Subst
su) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su Reft
r
  subst Subst
su (RProp [(Symbol, RType RTyCon RTyVar ())]
ss RType RTyCon RTyVar Reft
r)  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => Subst -> a -> a
subst Subst
su) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su RType RTyCon RTyVar Reft
r


  substf :: (Symbol -> Expr) -> RRProp Reft -> RRProp Reft
substf Symbol -> Expr
f (RProp [(Symbol, RType RTyCon RTyVar ())]
ss (RHole Reft
r)) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Reft
r
  substf Symbol -> Expr
f (RProp [(Symbol, RType RTyCon RTyVar ())]
ss RType RTyCon RTyVar Reft
r) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f RType RTyCon RTyVar Reft
r

  substa :: (Symbol -> Symbol) -> RRProp Reft -> RRProp Reft
substa Symbol -> Symbol
f (RProp [(Symbol, RType RTyCon RTyVar ())]
ss (RHole Reft
r)) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f Reft
r
  substa Symbol -> Symbol
f (RProp [(Symbol, RType RTyCon RTyVar ())]
ss RType RTyCon RTyVar Reft
r) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar ())]
ss) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f RType RTyCon RTyVar Reft
r


-------------------------------------------------------------------------------
-- | Reftable Instances -------------------------------------------------------
-------------------------------------------------------------------------------

instance (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
    => Reftable (RType RTyCon RTyVar r) where
  isTauto :: RType RTyCon RTyVar r -> Bool
isTauto     = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial
  ppTy :: RType RTyCon RTyVar r -> Doc -> Doc
ppTy        = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"ppTy RProp Reftable"
  toReft :: RType RTyCon RTyVar r -> Reft
toReft      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"toReft on RType"
  params :: RType RTyCon RTyVar r -> [Symbol]
params      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"params on RType"
  bot :: RType RTyCon RTyVar r -> RType RTyCon RTyVar r
bot         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"bot on RType"
  ofReft :: Reft -> RType RTyCon RTyVar r
ofReft      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"ofReft on RType"


instance Reftable (RType BTyCon BTyVar (UReft Reft)) where
  isTauto :: RType BTyCon BTyVar (UReft Reft) -> Bool
isTauto     = forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial
  top :: RType BTyCon BTyVar (UReft Reft)
-> RType BTyCon BTyVar (UReft Reft)
top RType BTyCon BTyVar (UReft Reft)
t       = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall r. Reftable r => r -> r
top RType BTyCon BTyVar (UReft Reft)
t
  ppTy :: RType BTyCon BTyVar (UReft Reft) -> Doc -> Doc
ppTy        = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"ppTy RProp Reftable"
  toReft :: RType BTyCon BTyVar (UReft Reft) -> Reft
toReft      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"toReft on RType"
  params :: RType BTyCon BTyVar (UReft Reft) -> [Symbol]
params      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"params on RType"
  bot :: RType BTyCon BTyVar (UReft Reft)
-> RType BTyCon BTyVar (UReft Reft)
bot         = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"bot on RType"
  ofReft :: Reft -> RType BTyCon BTyVar (UReft Reft)
ofReft      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"ofReft on RType"



-- MOVE TO TYPES
instance Fixpoint String where
  toFix :: String -> Doc
toFix = String -> Doc
text

-- MOVE TO TYPES
instance Fixpoint Class where
  toFix :: Class -> Doc
toFix = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> String
GM.showPpr

-- MOVE TO TYPES
class FreeVar a v where
  freeVars :: a -> [v]

-- MOVE TO TYPES
instance FreeVar RTyCon RTyVar where
  freeVars :: RTyCon -> [RTyVar]
freeVars = (TyVar -> RTyVar
RTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [TyVar]
GM.tyConTyVarsDef forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon -> TyCon
rtc_tc

-- MOVE TO TYPES
instance FreeVar BTyCon BTyVar where
  freeVars :: BTyCon -> [BTyVar]
freeVars BTyCon
_ = []

-- Eq Instances ------------------------------------------------------

-- MOVE TO TYPES
instance (Eq c, Eq tv, Hashable tv, PPrint tv, TyConable c, PPrint c, Reftable (RTProp c tv ()))
      => Eq (RType c tv ()) where
  == :: RType c tv () -> RType c tv () -> Bool
(==) = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort forall k v. HashMap k v
M.empty

eqRSort :: (Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k, Reftable (RTProp a k ()))
        => M.HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort :: forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m (RAllP PVU a k
_ RType a k ()
t) (RAllP PVU a k
_ RType a k ()
t')
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t RType a k ()
t'
eqRSort HashMap k k
m (RAllP PVU a k
_ RType a k ()
t) RType a k ()
t'
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t RType a k ()
t'
eqRSort HashMap k k
m (RAllT RTVU a k
a RType a k ()
t ()
_) (RAllT RTVU a k
a' RType a k ()
t' ()
_)
  | RTVU a k
a forall a. Eq a => a -> a -> Bool
== RTVU a k
a'
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t RType a k ()
t'
  | Bool
otherwise
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (forall tv s. RTVar tv s -> tv
ty_var_value RTVU a k
a') (forall tv s. RTVar tv s -> tv
ty_var_value RTVU a k
a) HashMap k k
m) RType a k ()
t RType a k ()
t'
eqRSort HashMap k k
m (RAllT RTVU a k
_ RType a k ()
t ()
_) RType a k ()
t'
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t RType a k ()
t'
eqRSort HashMap k k
m RType a k ()
t (RAllT RTVU a k
_ RType a k ()
t' ()
_)
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t RType a k ()
t'
eqRSort HashMap k k
m (RFun Symbol
_ RFInfo
_ RType a k ()
t1 RType a k ()
t2 ()
_) (RFun Symbol
_ RFInfo
_ RType a k ()
t1' RType a k ()
t2' ()
_)
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t1 RType a k ()
t1' Bool -> Bool -> Bool
&& forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t2 RType a k ()
t2'
eqRSort HashMap k k
m (RAppTy RType a k ()
t1 RType a k ()
t2 ()
_) (RAppTy RType a k ()
t1' RType a k ()
t2' ()
_)
  = forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t1 RType a k ()
t1' Bool -> Bool -> Bool
&& forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m RType a k ()
t2 RType a k ()
t2'
eqRSort HashMap k k
m (RApp a
c [RType a k ()]
ts [RTProp a k ()]
_ ()
_) (RApp a
c' [RType a k ()]
ts' [RTProp a k ()]
_ ()
_)
  = a
c forall a. Eq a => a -> a -> Bool
== a
c' Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType a k ()]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType a k ()]
ts' Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a k.
(Eq a, Eq k, Hashable k, TyConable a, PPrint a, PPrint k,
 Reftable (RTProp a k ())) =>
HashMap k k -> RType a k () -> RType a k () -> Bool
eqRSort HashMap k k
m) [RType a k ()]
ts [RType a k ()]
ts')
eqRSort HashMap k k
m (RVar k
a ()
_) (RVar k
a' ()
_)
  = k
a forall a. Eq a => a -> a -> Bool
== forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault k
a' k
a' HashMap k k
m
eqRSort HashMap k k
_ (RHole ()
_) RType a k ()
_
  = Bool
True
eqRSort HashMap k k
_ RType a k ()
_         (RHole ()
_)
  = Bool
True
eqRSort HashMap k k
_ RType a k ()
_ RType a k ()
_
  = Bool
False

--------------------------------------------------------------------------------
-- | Wrappers for GHC Type Elements --------------------------------------------
--------------------------------------------------------------------------------

instance Eq RTyVar where
  -- FIXME: need to compare unique and string because we reuse
  -- uniques in stringTyVar and co.
  RTV TyVar
α == :: RTyVar -> RTyVar -> Bool
== RTV TyVar
α' = TyVar
α forall a. Eq a => a -> a -> Bool
== TyVar
α' Bool -> Bool -> Bool
&& forall a. NamedThing a => a -> OccName
getOccName TyVar
α forall a. Eq a => a -> a -> Bool
== forall a. NamedThing a => a -> OccName
getOccName TyVar
α'

instance Ord RTyVar where
  compare :: RTyVar -> RTyVar -> Ordering
compare (RTV TyVar
α) (RTV TyVar
α') = case forall a. Ord a => a -> a -> Ordering
compare TyVar
α TyVar
α' of
    Ordering
EQ -> forall a. Ord a => a -> a -> Ordering
compare (forall a. NamedThing a => a -> OccName
getOccName TyVar
α) (forall a. NamedThing a => a -> OccName
getOccName TyVar
α')
    Ordering
o  -> Ordering
o

instance Hashable RTyVar where
  hashWithSalt :: Int -> RTyVar -> Int
hashWithSalt Int
i (RTV TyVar
α) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i TyVar
α

-- TyCon isn't comparable
--instance Ord RTyCon where
--  compare x y = compare (rtc_tc x) (rtc_tc y)

instance Hashable RTyCon where
  hashWithSalt :: Int -> RTyCon -> Int
hashWithSalt Int
i = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon -> TyCon
rtc_tc

--------------------------------------------------------------------------------
-- | Helper Functions (RJ: Helping to do what?) --------------------------------
--------------------------------------------------------------------------------

rVar :: Monoid r => TyVar -> RType c RTyVar r
rVar :: forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar   = (forall c tv r. tv -> r -> RType c tv r
`RVar` forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> RTyVar
RTV

rTyVar :: TyVar -> RTyVar
rTyVar :: TyVar -> RTyVar
rTyVar = TyVar -> RTyVar
RTV

updateRTVar :: Monoid r => RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar :: forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar (RTV TyVar
a) RTVInfo i
_) = forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (TyVar -> RTyVar
RTV TyVar
a) (forall r. Monoid r => TyVar -> RTVInfo (RRType r)
rTVarInfo TyVar
a)

rTVar :: Monoid r => TyVar -> RTVar RTyVar (RRType r)
rTVar :: forall r. Monoid r => TyVar -> RTVar RTyVar (RRType r)
rTVar TyVar
a = forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (TyVar -> RTyVar
RTV TyVar
a) (forall r. Monoid r => TyVar -> RTVInfo (RRType r)
rTVarInfo TyVar
a)

bTVar :: Monoid r => TyVar -> RTVar BTyVar (BRType r)
bTVar :: forall r. Monoid r => TyVar -> RTVar BTyVar (BRType r)
bTVar TyVar
a = forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar (Symbol -> BTyVar
BTV (forall a. Symbolic a => a -> Symbol
symbol TyVar
a)) (forall r. Monoid r => TyVar -> RTVInfo (BRType r)
bTVarInfo TyVar
a)

bTVarInfo :: Monoid r => TyVar -> RTVInfo (BRType r)
bTVarInfo :: forall r. Monoid r => TyVar -> RTVInfo (BRType r)
bTVarInfo = forall s. (Type -> s) -> TyVar -> RTVInfo s
mkTVarInfo forall r. Monoid r => Type -> BRType r
kindToBRType

rTVarInfo :: Monoid r => TyVar -> RTVInfo (RRType r)
rTVarInfo :: forall r. Monoid r => TyVar -> RTVInfo (RRType r)
rTVarInfo = forall s. (Type -> s) -> TyVar -> RTVInfo s
mkTVarInfo forall r. Monoid r => Type -> RRType r
kindToRType

mkTVarInfo :: (Kind -> s) -> TyVar -> RTVInfo s
mkTVarInfo :: forall s. (Type -> s) -> TyVar -> RTVInfo s
mkTVarInfo Type -> s
k2t TyVar
a = RTVInfo
  { rtv_name :: Symbol
rtv_name   = forall a. Symbolic a => a -> Symbol
symbol    forall a b. (a -> b) -> a -> b
$ TyVar -> Name
varName TyVar
a
  , rtv_kind :: s
rtv_kind   = Type -> s
k2t       forall a b. (a -> b) -> a -> b
$ TyVar -> Type
tyVarKind TyVar
a
  , rtv_is_val :: Bool
rtv_is_val = Type -> Bool
isValKind forall a b. (a -> b) -> a -> b
$ TyVar -> Type
tyVarKind TyVar
a
  , rtv_is_pol :: Bool
rtv_is_pol = Bool
True
  }

kindToRType :: Monoid r => Type -> RRType r
kindToRType :: forall r. Monoid r => Type -> RRType r
kindToRType = forall z. (Type -> z) -> Type -> z
kindToRType_ forall r. Monoid r => Type -> RRType r
ofType

kindToBRType :: Monoid r => Type -> BRType r
kindToBRType :: forall r. Monoid r => Type -> BRType r
kindToBRType = forall z. (Type -> z) -> Type -> z
kindToRType_ forall r. Monoid r => Type -> BRType r
bareOfType

kindToRType_ :: (Type -> z) -> Type -> z
kindToRType_ :: forall z. (Type -> z) -> Type -> z
kindToRType_ Type -> z
ofType'       = Type -> z
ofType' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
go
  where
    go :: Type -> Type
go Type
t
     | Type
t forall a. Eq a => a -> a -> Bool
== Type
typeSymbolKind = Type
stringTy
     | Type
t forall a. Eq a => a -> a -> Bool
== Type
naturalTy      = Type
intTy
     | Bool
otherwise           = Type
t

isValKind :: Kind -> Bool
isValKind :: Type -> Bool
isValKind Type
x0 =
    let x :: Type
x = Type -> Type
expandTypeSynonyms Type
x0
     in Type
x forall a. Eq a => a -> a -> Bool
== Type
naturalTy Bool -> Bool -> Bool
|| Type
x forall a. Eq a => a -> a -> Bool
== Type
typeSymbolKind

bTyVar :: Symbol -> BTyVar
bTyVar :: Symbol -> BTyVar
bTyVar      = Symbol -> BTyVar
BTV

symbolRTyVar :: Symbol -> RTyVar
symbolRTyVar :: Symbol -> RTyVar
symbolRTyVar = TyVar -> RTyVar
rTyVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TyVar
GM.symbolTyVar

bareRTyVar :: BTyVar -> RTyVar
bareRTyVar :: BTyVar -> RTyVar
bareRTyVar (BTV Symbol
tv) = Symbol -> RTyVar
symbolRTyVar Symbol
tv

normalizePds :: (OkRT c tv r) => RType c tv r -> RType c tv r
normalizePds :: forall c tv r. OkRT c tv r => RType c tv r -> RType c tv r
normalizePds RType c tv r
t = forall (t :: * -> *) c tv r.
Foldable t =>
t (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
addPds [PVar (RType c tv ())]
ps RType c tv r
t'
  where
    (RType c tv r
t', [PVar (RType c tv ())]
ps)   = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t

rPred :: PVar (RType c tv ()) -> RType c tv r -> RType c tv r
rPred :: forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
rPred     = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP

rEx :: Foldable t
    => t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
rEx :: forall (t :: * -> *) c tv r.
Foldable t =>
t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
rEx t (Symbol, RType c tv r)
xts RType c tv r
rt = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Symbol
x, RType c tv r
tx) RType c tv r
t -> forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x RType c tv r
tx RType c tv r
t) RType c tv r
rt t (Symbol, RType c tv r)
xts

rApp :: TyCon
     -> [RType RTyCon tv r]
     -> [RTProp RTyCon tv r]
     -> r
     -> RType RTyCon tv r
rApp :: forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> RTyCon
tyConRTyCon TyCon
c)

gApp :: TyCon -> [RTyVar] -> [PVar a] -> SpecType
gApp :: forall a. TyCon -> [RTyVar] -> [PVar a] -> SpecType
gApp TyCon
tc [RTyVar]
αs [PVar a]
πs = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
tc
                  [forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar TyVar
α | RTV TyVar
α <- [RTyVar]
αs]
                  (forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PVar t -> UReft Reft
pdVarReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar a]
πs)
                  forall a. Monoid a => a
mempty

pdVarReft :: PVar t -> UReft Reft
pdVarReft :: forall t. PVar t -> UReft Reft
pdVarReft = (\Predicate
p -> forall r. r -> Predicate -> UReft r
MkUReft forall a. Monoid a => a
mempty Predicate
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PVar t -> Predicate
pdVar

tyConRTyCon :: TyCon -> RTyCon
tyConRTyCon :: TyCon -> RTyCon
tyConRTyCon TyCon
c = TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] (TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
mkTyConInfo TyCon
c [] [] forall a. Maybe a
Nothing)

-- bApp :: (Monoid r) => TyCon -> [BRType r] -> BRType r
bApp :: TyCon -> [BRType r] -> [BRProp r] -> r -> BRType r
bApp :: forall r. TyCon -> [BRType r] -> [BRProp r] -> r -> BRType r
bApp TyCon
c = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp (TyCon -> BTyCon
tyConBTyCon TyCon
c)

tyConBTyCon :: TyCon -> BTyCon
tyConBTyCon :: TyCon -> BTyCon
tyConBTyCon = LocSymbol -> BTyCon
mkBTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCon -> Symbol
tyConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedThing a => a -> Located a
GM.locNamedThing
-- tyConBTyCon = mkBTyCon . fmap symbol . locNamedThing

--- NV TODO : remove this code!!!

addPds :: Foldable t
       => t (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
addPds :: forall (t :: * -> *) c tv r.
Foldable t =>
t (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
addPds t (PVar (RType c tv ()))
ps (RAllT RTVU c tv
v RType c tv r
t r
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v (forall (t :: * -> *) c tv r.
Foldable t =>
t (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
addPds t (PVar (RType c tv ()))
ps RType c tv r
t) r
r
addPds t (PVar (RType c tv ()))
ps RType c tv r
t             = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
rPred) RType c tv r
t t (PVar (RType c tv ()))
ps

nlzP :: (OkRT c tv r) => [PVar (RType c tv ())] -> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP :: forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [PVar (RType c tv ())]
ps t :: RType c tv r
t@(RVar tv
_ r
_ )
 = (RType c tv r
t, [PVar (RType c tv ())]
ps)
nlzP [PVar (RType c tv ())]
ps (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r)
 = (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1' RType c tv r
t2' r
r, [PVar (RType c tv ())]
ps forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps1 forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps2)
  where (RType c tv r
t1', [PVar (RType c tv ())]
ps1) = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t1
        (RType c tv r
t2', [PVar (RType c tv ())]
ps2) = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t2
nlzP [PVar (RType c tv ())]
ps (RAppTy RType c tv r
t1 RType c tv r
t2 r
r)
 = (forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1' RType c tv r
t2' r
r, [PVar (RType c tv ())]
ps forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps1 forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps2)
  where (RType c tv r
t1', [PVar (RType c tv ())]
ps1) = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t1
        (RType c tv r
t2', [PVar (RType c tv ())]
ps2) = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t2
nlzP [PVar (RType c tv ())]
ps (RAllT RTVU c tv
v RType c tv r
t r
r)
 = (forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
v RType c tv r
t' r
r, [PVar (RType c tv ())]
ps forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps')
  where (RType c tv r
t', [PVar (RType c tv ())]
ps') = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t
nlzP [PVar (RType c tv ())]
ps t :: RType c tv r
t@RApp{}
 = (RType c tv r
t, [PVar (RType c tv ())]
ps)
nlzP [PVar (RType c tv ())]
ps (RAllP PVar (RType c tv ())
p RType c tv r
t)
 = (RType c tv r
t', [PVar (RType c tv ())
p] forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps')
  where (RType c tv r
t', [PVar (RType c tv ())]
ps') = forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t
nlzP [PVar (RType c tv ())]
ps t :: RType c tv r
t@REx{}
 = (RType c tv r
t, [PVar (RType c tv ())]
ps)
nlzP [PVar (RType c tv ())]
ps t :: RType c tv r
t@(RRTy [(Symbol, RType c tv r)]
_ r
_ Oblig
_ RType c tv r
t')
 = (RType c tv r
t, [PVar (RType c tv ())]
ps forall a. [a] -> [a] -> [a]
++ [PVar (RType c tv ())]
ps')
 where ps' :: [PVar (RType c tv ())]
ps' = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall c tv r.
OkRT c tv r =>
[PVar (RType c tv ())]
-> RType c tv r -> (RType c tv r, [PVar (RType c tv ())])
nlzP [] RType c tv r
t'
nlzP [PVar (RType c tv ())]
ps t :: RType c tv r
t@RAllE{}
 = (RType c tv r
t, [PVar (RType c tv ())]
ps)
nlzP [PVar (RType c tv ())]
_ RType c tv r
t
 = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"RefType.nlzP: cannot handle " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RType c tv r
t

strengthenRefTypeGen, strengthenRefType ::
         (  OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) c
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) tv
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         ) => RType c tv r -> RType c tv r -> RType c tv r

strengthenRefType_ ::
         ( OkRT c tv r
         , FreeVar c tv
         , SubsTy tv (RType c tv ()) (RType c tv ())
         , SubsTy tv (RType c tv ()) c
         , SubsTy tv (RType c tv ()) r
         , SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))
         , SubsTy tv (RType c tv ()) tv
         ) => (RType c tv r -> RType c tv r -> RType c tv r)
           ->  RType c tv r -> RType c tv r -> RType c tv r

strengthenRefTypeGen :: forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
strengthenRefTypeGen = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ forall {r} {c} {c} {tv} {tv}.
(TyConable c, TyConable c, PPrint tv, PPrint c, PPrint r,
 PPrint tv, PPrint c, Reftable r, Reftable (RTProp c tv r),
 Reftable (RTProp c tv ()), Reftable (RTProp c tv r),
 Reftable (RTProp c tv ()), Hashable tv, Hashable tv) =>
RType c tv r -> RType c tv r -> RType c tv r
f
  where
    f :: RType c tv r -> RType c tv r -> RType c tv r
f (RVar tv
v1 r
r1) RType c tv r
t  = forall c tv r. tv -> r -> RType c tv r
RVar tv
v1 (r
r1 forall r. Reftable r => r -> r -> r
`meet` forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RType c tv r
t))
    f RType c tv r
t (RVar tv
_ r
r1)  = RType c tv r
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` r
r1
    f RType c tv r
t1 RType c tv r
t2           = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"strengthenRefTypeGen on differently shaped types \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]"
                         (forall c tv r. OkRT c tv r => RType c tv r -> String
pprRaw RType c tv r
t1) (forall a. PPrint a => a -> String
showpp (forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t1)) (forall c tv r. OkRT c tv r => RType c tv r -> String
pprRaw RType c tv r
t2) (forall a. PPrint a => a -> String
showpp (forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t2))

pprRaw :: (OkRT c tv r) => RType c tv r -> String
pprRaw :: forall c tv r. OkRT c tv r => RType c tv r -> String
pprRaw = Doc -> String
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc Tidy
Full

{- [NOTE:StrengthenRefType] disabling the `meetable` check because

      (1) It requires the 'TCEmb TyCon' to deal with the fact that sometimes,
          GHC uses the "Family Instance" TyCon e.g. 'R:UniquePerson' and sometimes
          the vanilla TyCon App form, e.g. 'Unique Person'
      (2) We could pass in the TCEmb but that would break the 'Monoid' instance for
          RType. The 'Monoid' instance was was probably a bad idea to begin with,
          and we probably ought to do away with it entirely, but thats a battle I'll
          leave for another day.

    Consequently, its up to users of `strengthenRefType` (and associated functions)
    to make sure that the two types are compatible. For an example, see 'meetVarTypes'.
 -}

strengthenRefType :: forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType RType c tv r
t1 RType c tv r
t2
  -- | _meetable t1 t2
  = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ forall a b. a -> b -> a
const RType c tv r
t1 RType c tv r
t2
  -- | otherwise
  -- = panic Nothing msg
  -- where
  --   msg = printf "strengthen on differently shaped reftypes \nt1 = %s [shape = %s]\nt2 = %s [shape = %s]"
  --           (showpp t1) (showpp (toRSort t1)) (showpp t2) (showpp (toRSort t2))

_meetable :: (OkRT c tv r) => RType c tv r -> RType c tv r -> Bool
_meetable :: forall c tv r. OkRT c tv r => RType c tv r -> RType c tv r -> Bool
_meetable RType c tv r
t1 RType c tv r
t2 = forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t1 forall a. Eq a => a -> a -> Bool
== forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t2

strengthenRefType_ :: forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllT RTVar tv (RType c tv ())
a1 RType c tv r
t1 r
r1) (RAllT RTVar tv (RType c tv ())
a2 RType c tv r
t2 r
r2)
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar tv (RType c tv ())
a1 (forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
a2, forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t, RType c tv r
t) RType c tv r
t2)) (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
  where t :: RType c tv r
t = forall c tv r. tv -> r -> RType c tv r
RVar (forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
a1) forall a. Monoid a => a
mempty

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllT RTVar tv (RType c tv ())
a RType c tv r
t1 r
r1) RType c tv r
t2
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar tv (RType c tv ())
a (forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2) r
r1

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 (RAllT RTVar tv (RType c tv ())
a RType c tv r
t2 r
r2)
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar tv (RType c tv ())
a (forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2) r
r2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllP PVU c tv
p1 RType c tv r
t1) (RAllP PVU c tv
_ RType c tv r
t2)
  = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP PVU c tv
p1 forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllP PVU c tv
p RType c tv r
t1) RType c tv r
t2
  = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP PVU c tv
p forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 (RAllP PVU c tv
p RType c tv r
t2)
  = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP PVU c tv
p forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllE Symbol
x RType c tv r
tx RType c tv r
t1) (RAllE Symbol
y RType c tv r
ty RType c tv r
t2) | Symbol
x forall a. Eq a => a -> a -> Bool
== Symbol
y
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x (forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
tx RType c tv r
ty) forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAllE Symbol
x RType c tv r
tx RType c tv r
t1) RType c tv r
t2
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x RType c tv r
tx forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 (RAllE Symbol
x RType c tv r
tx RType c tv r
t2)
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x RType c tv r
tx forall a b. (a -> b) -> a -> b
$ forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RAppTy RType c tv r
t1 RType c tv r
t1' r
r1) (RAppTy RType c tv r
t2 RType c tv r
t2' r
r2)
  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t RType c tv r
t' (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
    where t :: RType c tv r
t  = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2
          t' :: RType c tv r
t' = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1' RType c tv r
t2'

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RFun Symbol
x1 RFInfo
i1 RType c tv r
t1 RType c tv r
t1' r
r1) (RFun Symbol
x2 RFInfo
i2 RType c tv r
t2 RType c tv r
t2' r
r2) =
  -- YL: Evidence that we need a Monoid instance for RFInfo?
  if Symbol
x2 forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol
    then forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x2 RFInfo
i1{permitTC :: Maybe Bool
permitTC = forall a. First a -> Maybe a
getFirst First Bool
b} RType c tv r
t RType c tv r
t1'' (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
    else forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x1 RFInfo
i1{permitTC :: Maybe Bool
permitTC = forall a. First a -> Maybe a
getFirst First Bool
b} RType c tv r
t RType c tv r
t2'' (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
    where t :: RType c tv r
t  = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2
          t1'' :: RType c tv r
t1'' = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 RType c tv r
t1' (Symbol
x1, Symbol -> Expr
EVar Symbol
x2)) RType c tv r
t2'
          t2'' :: RType c tv r
t2'' = forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1' (forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 RType c tv r
t2' (Symbol
x2, Symbol -> Expr
EVar Symbol
x1))
          b :: First Bool
b  = forall a. Maybe a -> First a
First (RFInfo -> Maybe Bool
permitTC RFInfo
i1) forall a. Semigroup a => a -> a -> a
<> forall a. Maybe a -> First a
First (RFInfo -> Maybe Bool
permitTC RFInfo
i2)

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f (RApp c
tid [RType c tv r]
t1s [RTProp c tv r]
rs1 r
r1) (RApp c
_ [RType c tv r]
t2s [RTProp c tv r]
rs2 r
r2)
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
tid [RType c tv r]
ts [RTProp c tv r]
rs (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
    where ts :: [RType c tv r]
ts  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall c tv r.
(OkRT c tv r, FreeVar c tv,
 SubsTy tv (RType c tv ()) (RType c tv ()),
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())),
 SubsTy tv (RType c tv ()) tv) =>
(RType c tv r -> RType c tv r -> RType c tv r)
-> RType c tv r -> RType c tv r -> RType c tv r
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f) [RType c tv r]
t1s [RType c tv r]
t2s
          rs :: [RTProp c tv r]
rs  = forall r. Reftable r => [r] -> [r] -> [r]
meets [RTProp c tv r]
rs1 [RTProp c tv r]
rs2

strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
_ (RVar tv
v1 r
r1)  (RVar tv
v2 r
r2) | tv
v1 forall a. Eq a => a -> a -> Bool
== tv
v2
  = forall c tv r. tv -> r -> RType c tv r
RVar tv
v1 (r
r1 forall r. Reftable r => r -> r -> r
`meet` r
r2)
strengthenRefType_ RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2
  = RType c tv r -> RType c tv r -> RType c tv r
f RType c tv r
t1 RType c tv r
t2

meets :: (F.Reftable r) => [r] -> [r] -> [r]
meets :: forall r. Reftable r => [r] -> [r] -> [r]
meets [] [r]
rs                 = [r]
rs
meets [r]
rs []                 = [r]
rs
meets [r]
rs [r]
rs'
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [r]
rs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [r]
rs' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall r. Reftable r => r -> r -> r
meet [r]
rs [r]
rs'
  | Bool
otherwise               = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"meets: unbalanced rs"

strengthen :: Reftable r => RType c tv r -> r -> RType c tv r
strengthen :: forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r)   r
r' = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs   (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthen (RVar tv
a r
r)         r
r' = forall c tv r. tv -> r -> RType c tv r
RVar tv
a         (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthen (RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 r
r) r
r' = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
b RFInfo
i RType c tv r
t1 RType c tv r
t2 (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthen (RAppTy RType c tv r
t1 RType c tv r
t2 r
r)   r
r' = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t1 RType c tv r
t2   (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthen (RAllT RTVU c tv
a RType c tv r
t r
r)      r
r' = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a RType c tv r
t      (r
r forall r. Reftable r => r -> r -> r
`F.meet` r
r')
strengthen RType c tv r
t                  r
_  = RType c tv r
t

quantifyRTy :: (Monoid r, Eq tv) => [RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
quantifyRTy :: forall r tv c.
(Monoid r, Eq tv) =>
[RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
quantifyRTy [RTVar tv (RType c tv ())]
tvs RType c tv r
ty = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {r} {c} {tv}.
Monoid r =>
RTVU c tv -> RType c tv r -> RType c tv r
rAllT RType c tv r
ty [RTVar tv (RType c tv ())]
tvs
  where rAllT :: RTVU c tv -> RType c tv r -> RType c tv r
rAllT RTVU c tv
a RType c tv r
t = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a RType c tv r
t forall a. Monoid a => a
mempty

quantifyFreeRTy :: (Monoid r, Eq tv) => RType c tv r -> RType c tv r
quantifyFreeRTy :: forall r tv c. (Monoid r, Eq tv) => RType c tv r -> RType c tv r
quantifyFreeRTy RType c tv r
ty = forall r tv c.
(Monoid r, Eq tv) =>
[RTVar tv (RType c tv ())] -> RType c tv r -> RType c tv r
quantifyRTy (forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
ty) RType c tv r
ty


-------------------------------------------------------------------------
addTyConInfo :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
             => TCEmb TyCon
             -> TyConMap
             -> RRType r
             -> RRType r
-------------------------------------------------------------------------
addTyConInfo :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo TCEmb TyCon
tce TyConMap
tyi = forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
expandRApp TCEmb TyCon
tce TyConMap
tyi)

-------------------------------------------------------------------------
expandRApp :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RRProp r))
           => TCEmb TyCon -> TyConMap -> RRType r -> RRType r
-------------------------------------------------------------------------
expandRApp :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
expandRApp TCEmb TyCon
tce TyConMap
tyi t :: RRType r
t@RApp{} = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
rc' [RRType r]
ts [RRProp r]
rs' r
r
  where
    RApp RTyCon
rc [RRType r]
ts [RRProp r]
rs r
r            = RRType r
t
    (RTyCon
rc', [RPVar]
_)                   = forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
appRTyCon TCEmb TyCon
tce TyConMap
tyi RTyCon
rc [RRType r]
as
    pvs :: [RPVar]
pvs                        = RTyCon -> [RPVar]
rTyConPVs RTyCon
rc'
    rs' :: [RRProp r]
rs'                        = forall b a. b -> ([a] -> b) -> [a] -> b
applyNonNull [RRProp r]
rs0 (forall a r c tv.
(Fixpoint a, Reftable r) =>
a
-> [PVar (RType c tv ())]
-> [Ref (RType c tv ()) (RType c tv r)]
-> [Ref (RType c tv ()) (RType c tv r)]
rtPropPV RTyCon
rc [RPVar]
pvs) [RRProp r]
rs
    rs0 :: [RRProp r]
rs0                        = forall c tv r.
(OkRT c tv r, SubsTy tv (RType c tv ()) c,
 SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
PVar (RType c tv ()) -> Ref (RType c tv ()) (RType c tv r)
rtPropTop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RPVar]
pvs
    n :: Int
n                          = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVar]
fVs
    fVs :: [TyVar]
fVs                        = TyCon -> [TyVar]
GM.tyConTyVarsDef forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
rc
    as :: [RRType r]
as                         = forall a. Int -> [a] -> [a] -> [a]
choosen Int
n [RRType r]
ts (forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVar]
fVs)
expandRApp TCEmb TyCon
_ TyConMap
_ RRType r
t               = RRType r
t

choosen :: Int -> [a] -> [a] -> [a]
choosen :: forall a. Int -> [a] -> [a] -> [a]
choosen Int
0 [a]
_ [a]
_           = []
choosen Int
i (a
x:[a]
xs) (a
_:[a]
ys) = a
xforall a. a -> [a] -> [a]
:forall a. Int -> [a] -> [a] -> [a]
choosen (Int
iforall a. Num a => a -> a -> a
-Int
1) [a]
xs [a]
ys
choosen Int
i []     (a
y:[a]
ys) = a
yforall a. a -> [a] -> [a]
:forall a. Int -> [a] -> [a] -> [a]
choosen (Int
iforall a. Num a => a -> a -> a
-Int
1) [] [a]
ys
choosen Int
_ [a]
_ [a]
_           = forall a. Maybe SrcSpan -> String -> a
impossible forall a. Maybe a
Nothing String
"choosen: this cannot happen"


rtPropTop
  :: (OkRT c tv r,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
   => PVar (RType c tv ()) -> Ref (RType c tv ()) (RType c tv r)
rtPropTop :: forall c tv r.
(OkRT c tv r, SubsTy tv (RType c tv ()) c,
 SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
PVar (RType c tv ()) -> Ref (RType c tv ()) (RType c tv r)
rtPropTop PVar (RType c tv ())
pv = case forall t. PVar t -> PVKind t
ptype PVar (RType c tv ())
pv of
                 PVProp RType c tv ()
t -> forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xts forall a b. (a -> b) -> a -> b
$ forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType c tv ()
t
                 PVKind (RType c tv ())
PVHProp  -> forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
xts forall a. Monoid a => a
mempty
               where
                 xts :: [(Symbol, RType c tv ())]
xts      =  forall t. PVar t -> [(Symbol, t)]
pvArgs PVar (RType c tv ())
pv

rtPropPV :: (Fixpoint a, Reftable r)
         => a
         -> [PVar (RType c tv ())]
         -> [Ref (RType c tv ()) (RType c tv r)]
         -> [Ref (RType c tv ()) (RType c tv r)]
rtPropPV :: forall a r c tv.
(Fixpoint a, Reftable r) =>
a
-> [PVar (RType c tv ())]
-> [Ref (RType c tv ()) (RType c tv r)]
-> [Ref (RType c tv ()) (RType c tv r)]
rtPropPV a
_rc = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall r c tv.
Reftable r =>
PVar (RType c tv ())
-> Ref (RType c tv ()) (RType c tv r)
-> Ref (RType c tv ()) (RType c tv r)
mkRTProp

mkRTProp :: Reftable r
         => PVar (RType c tv ())
         -> Ref (RType c tv ()) (RType c tv r)
         -> Ref (RType c tv ()) (RType c tv r)
mkRTProp :: forall r c tv.
Reftable r =>
PVar (RType c tv ())
-> Ref (RType c tv ()) (RType c tv r)
-> Ref (RType c tv ()) (RType c tv r)
mkRTProp PVar (RType c tv ())
pv (RProp [(Symbol, RType c tv ())]
ss (RHole r
r))
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
ss forall a b. (a -> b) -> a -> b
$ forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort (forall t. PVar t -> t
pvType PVar (RType c tv ())
pv) forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` r
r

mkRTProp PVar (RType c tv ())
pv (RProp [(Symbol, RType c tv ())]
ss RType c tv r
t)
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RType c tv ())
pv) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType c tv ())]
ss
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType c tv ())]
ss RType c tv r
t
  | Bool
otherwise
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall t. PVar t -> [(Symbol, t)]
pvArgs PVar (RType c tv ())
pv) RType c tv r
t

pvArgs :: PVar t -> [(Symbol, t)]
pvArgs :: forall t. PVar t -> [(Symbol, t)]
pvArgs PVar t
pv = [(Symbol
s, t
t) | (t
t, Symbol
s, Expr
_) <- forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
pv]

{- | [NOTE:FamInstPredVars] related to [NOTE:FamInstEmbeds]
     See tests/datacon/pos/T1446.hs
     The function txRefSort converts

        Int<p>              ===> {v:Int | p v}

     which is fine, but also converts

        Field<q> Blob a     ===> {v:Field Blob a | q v}

     which is NOT ok, because q expects a different arg.

     The above happens because, thanks to instance-family stuff,
     LH doesn't realize that q is actually an ARG of Field Blob
     Note that Field itself has no args, but Field Blob does...

     That is, it is not enough to store the refined `TyCon` info,
     solely in the `RTyCon` as with family instances, you need BOTH
     the `TyCon` and the args to determine the extra info.

     We do so in `TyConMap`, and by crucially extending

     @RefType.appRTyCon@ whose job is to use the Refined @TyCon@
     that is, the @RTyCon@ generated from the @TyConP@ to strengthen
     individual occurrences of the TyCon applied to various arguments.

 -}

appRTyCon :: (ToTypeable r) => TCEmb TyCon -> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
appRTyCon :: forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap -> RTyCon -> [RRType r] -> (RTyCon, [RPVar])
appRTyCon TCEmb TyCon
tce TyConMap
tyi RTyCon
rc [RRType r]
ts = forall a. PPrint a => String -> a -> a
F.notracepp String
_msg (RTyCon
resTc, [RPVar]
ps'')
  where
    _msg :: String
_msg  = String
"appRTyCon-family: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp (TyCon -> Bool
Ghc.isFamilyTyCon TyCon
c, TyCon -> Int
Ghc.tyConRealArity TyCon
c, forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType r]
ts)
    resTc :: RTyCon
resTc = TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon TyCon
c [RPVar]
ps'' (RTyCon -> TyConInfo
rtc_info RTyCon
rc'')
    c :: TyCon
c     = RTyCon -> TyCon
rtc_tc RTyCon
rc

    (RTyCon
rc', [RPVar]
ps') = TyConMap -> RTyCon -> [Sort] -> (RTyCon, [RPVar])
rTyConWithPVars TyConMap
tyi RTyCon
rc (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType r]
ts)
    -- TODO:faminst-preds rc'   = M.lookupDefault rc c (tcmTyRTy tyi)
    -- TODO:faminst-preds ps'   = rTyConPVs rc'

    -- TODO:faminst-preds: these substitutions may be WRONG if we are using FAMINST.
    ps'' :: [RPVar]
ps''  = forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts (forall a b. [a] -> [b] -> [(a, b)]
zip (TyVar -> RTyVar
RTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVar]
αs) [RType RTyCon RTyVar ()]
ts') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RPVar]
ps'
      where
        ts' :: [RType RTyCon RTyVar ()]
ts' = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RRType r]
ts then forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVar]
βs else forall c tv r. RType c tv r -> RType c tv ()
toRSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType r]
ts
        αs :: [TyVar]
αs  = TyCon -> [TyVar]
GM.tyConTyVarsDef (RTyCon -> TyCon
rtc_tc RTyCon
rc')
        βs :: [TyVar]
βs  = TyCon -> [TyVar]
GM.tyConTyVarsDef TyCon
c

    rc'' :: RTyCon
rc''  = if TCEmb TyCon -> RTyCon -> Bool
isNumeric TCEmb TyCon
tce RTyCon
rc' then RTyCon -> RTyCon
addNumSizeFun RTyCon
rc' else RTyCon
rc'

rTyConWithPVars :: TyConMap -> RTyCon -> [F.Sort] -> (RTyCon, [RPVar])
rTyConWithPVars :: TyConMap -> RTyCon -> [Sort] -> (RTyCon, [RPVar])
rTyConWithPVars TyConMap
tyi RTyCon
rc [Sort]
ts = case TyConMap -> RTyCon -> [Sort] -> Maybe RTyCon
famInstTyConMb TyConMap
tyi RTyCon
rc [Sort]
ts of
  Just RTyCon
fiRc    -> (RTyCon
rc', RTyCon -> [RPVar]
rTyConPVs RTyCon
fiRc)       -- use the PVars from the family-instance TyCon
  Maybe RTyCon
Nothing      -> (RTyCon
rc', [RPVar]
ps')                  -- use the PVars from the origin          TyCon
  where
    (RTyCon
rc', [RPVar]
ps') = TyConMap -> RTyCon -> (RTyCon, [RPVar])
plainRTyConPVars TyConMap
tyi RTyCon
rc

-- | @famInstTyConMb rc args@ uses the @RTyCon@ AND @args@ to see if
--   this is a family instance @RTyCon@, and if so, returns it.
--   see [NOTE:FamInstPredVars]
--   eg: 'famInstTyConMb tyi Field [Blob, a]' should give 'Just R:FieldBlob'

famInstTyConMb :: TyConMap -> RTyCon -> [F.Sort] -> Maybe RTyCon
famInstTyConMb :: TyConMap -> RTyCon -> [Sort] -> Maybe RTyCon
famInstTyConMb TyConMap
tyi RTyCon
rc [Sort]
ts = do
  let c :: TyCon
c = RTyCon -> TyCon
rtc_tc RTyCon
rc
  Int
n    <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyCon
c      (TyConMap -> HashMap TyCon Int
tcmFtcArity TyConMap
tyi)
  forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (TyCon
c, forall a. Int -> [a] -> [a]
take Int
n [Sort]
ts) (TyConMap -> HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy    TyConMap
tyi)

famInstTyConType :: Ghc.TyCon -> Maybe Ghc.Type
famInstTyConType :: TyCon -> Maybe Type
famInstTyConType TyCon
c = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyCon -> [Type] -> Type
Ghc.mkTyConApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> Maybe (TyCon, [Type])
famInstArgs TyCon
c

-- | @famInstArgs c@ destructs a family-instance @TyCon@ into its components, e.g.
--   e.g. 'famInstArgs R:FieldBlob' is @(Field, [Blob])@

famInstArgs :: Ghc.TyCon -> Maybe (Ghc.TyCon, [Ghc.Type])
famInstArgs :: TyCon -> Maybe (TyCon, [Type])
famInstArgs TyCon
c = case TyCon -> Maybe (TyCon, [Type])
Ghc.tyConFamInst_maybe TyCon
c of
    Just (TyCon
c', [Type]
ts) -> forall a. PPrint a => String -> a -> a
F.notracepp (String
"famInstArgs: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (TyCon
c, Int
cArity, [Type]
ts))
                     forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (TyCon
c', forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts forall a. Num a => a -> a -> a
- Int
cArity) [Type]
ts)
    Maybe (TyCon, [Type])
Nothing       -> forall a. Maybe a
Nothing
    where
      cArity :: Int
cArity      = TyCon -> Int
Ghc.tyConRealArity TyCon
c

-- TODO:faminst-preds: case Ghc.tyConFamInst_maybe c of
-- TODO:faminst-preds:   Just (c', ts) -> F.tracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts))
-- TODO:faminst-preds:                    $ Just (famInstType (Ghc.tyConArity c) c' ts)
-- TODO:faminst-preds:   Nothing       -> Nothing

-- TODO:faminst-preds: famInstType :: Int -> Ghc.TyCon -> [Ghc.Type] -> Ghc.Type
-- TODO:faminst-preds: famInstType n c ts = Ghc.mkTyConApp c (take (length ts - n) ts)




-- | @plainTyConPVars@ uses the @TyCon@ to return the
--   "refined" @RTyCon@ and @RPVars@ from the refined
--   'data' definition for the @TyCon@, e.g. will use
--   'List Int' to return 'List<p> Int' (if List has an abs-ref).
plainRTyConPVars :: TyConMap -> RTyCon -> (RTyCon, [RPVar])
plainRTyConPVars :: TyConMap -> RTyCon -> (RTyCon, [RPVar])
plainRTyConPVars TyConMap
tyi RTyCon
rc = (RTyCon
rc', RTyCon -> [RPVar]
rTyConPVs RTyCon
rc')
  where
    rc' :: RTyCon
rc'                   = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault RTyCon
rc (RTyCon -> TyCon
rtc_tc RTyCon
rc) (TyConMap -> HashMap TyCon RTyCon
tcmTyRTy TyConMap
tyi)



-- RJ: The code of `isNumeric` is incomprehensible.
-- Please fix it to use intSort instead of intFTyCon
isNumeric :: TCEmb TyCon -> RTyCon -> Bool
isNumeric :: TCEmb TyCon -> RTyCon -> Bool
isNumeric TCEmb TyCon
tce RTyCon
c = Sort -> Bool
F.isNumeric Sort
mySort
  where
    -- mySort      = M.lookupDefault def rc tce
    mySort :: Sort
mySort      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
def forall a b. (a, b) -> a
fst (forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
rc TCEmb TyCon
tce)
    def :: Sort
def         = FTycon -> Sort
FTC forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> FTycon
symbolFTycon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Located a
dummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Symbol
tyConName forall a b. (a -> b) -> a -> b
$ TyCon
rc
    rc :: TyCon
rc          = RTyCon -> TyCon
rtc_tc RTyCon
c

addNumSizeFun :: RTyCon -> RTyCon
addNumSizeFun :: RTyCon -> RTyCon
addNumSizeFun RTyCon
c
  = RTyCon
c {rtc_info :: TyConInfo
rtc_info = (RTyCon -> TyConInfo
rtc_info RTyCon
c) {sizeFunction :: Maybe SizeFun
sizeFunction = forall a. a -> Maybe a
Just SizeFun
IdSizeFun } }


generalize :: (Eq tv, Monoid r) => RType c tv r -> RType c tv r
generalize :: forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
generalize RType c tv r
t = forall (t :: * -> *) (t1 :: * -> *) tv c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RType c tv ()), r)
-> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
mkUnivs (forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) (forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t)) [] RType c tv r
t

allTyVars :: (Ord tv) => RType c tv r -> [tv]
allTyVars :: forall tv c r. Ord tv => RType c tv r -> [tv]
allTyVars = forall a. Ord a => [a] -> [a]
sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars'

allTyVars' :: (Eq tv) => RType c tv r -> [tv]
allTyVars' :: forall tv c r. Eq tv => RType c tv r -> [tv]
allTyVars' RType c tv r
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall tv s. RTVar tv s -> tv
ty_var_value forall a b. (a -> b) -> a -> b
$ [RTVar tv (RType c tv ())]
vs forall a. [a] -> [a] -> [a]
++ [RTVar tv (RType c tv ())]
vs'
  where
    vs :: [RTVar tv (RType c tv ())]
vs      = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> a
fst3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall a b. (a -> b) -> a -> b
$ RType c tv r
t
    vs' :: [RTVar tv (RType c tv ())]
vs'     = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t


freeTyVars :: Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars :: forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars (RAllP PVU c tv
_ RType c tv r
t)       = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t
freeTyVars (RAllT RTVar tv (RType c tv ())
α RType c tv r
t r
_)     = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t forall a. Eq a => [a] -> [a] -> [a]
L.\\ [RTVar tv (RType c tv ())
α]
freeTyVars (RFun Symbol
_ RFInfo
_ RType c tv r
t RType c tv r
t' r
_) = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t forall a. Eq a => [a] -> [a] -> [a]
`L.union` forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t'
freeTyVars (RApp c
_ [RType c tv r]
ts [RTProp c tv r]
_ r
_)   = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars [RType c tv r]
ts
freeTyVars (RVar tv
α r
_)        = [forall tv s. tv -> RTVar tv s
makeRTVar tv
α]
freeTyVars (RAllE Symbol
_ RType c tv r
tx RType c tv r
t)    = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
tx forall a. Eq a => [a] -> [a] -> [a]
`L.union` forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t
freeTyVars (REx Symbol
_ RType c tv r
tx RType c tv r
t)      = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
tx forall a. Eq a => [a] -> [a] -> [a]
`L.union` forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t
freeTyVars (RExprArg Located Expr
_)      = []
freeTyVars (RAppTy RType c tv r
t RType c tv r
t' r
_)   = forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t forall a. Eq a => [a] -> [a] -> [a]
`L.union` forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars RType c tv r
t'
freeTyVars (RHole r
_)         = []
freeTyVars (RRTy [(Symbol, RType c tv r)]
e r
_ Oblig
_ RType c tv r
t)    = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars (RType c tv r
tforall a. a -> [a] -> [a]
:(forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
e))


tyClasses :: (OkRT RTyCon tv r) => RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses :: forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses (RAllP PVU RTyCon tv
_ RType RTyCon tv r
t)     = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t
tyClasses (RAllT RTVU RTyCon tv
_ RType RTyCon tv r
t r
_)   = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t
tyClasses (RAllE Symbol
_ RType RTyCon tv r
_ RType RTyCon tv r
t)   = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t
tyClasses (REx Symbol
_ RType RTyCon tv r
_ RType RTyCon tv r
t)     = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t
tyClasses (RFun Symbol
_ RFInfo
_ RType RTyCon tv r
t RType RTyCon tv r
t' r
_) = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t forall a. [a] -> [a] -> [a]
++ forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t'
tyClasses (RAppTy RType RTyCon tv r
t RType RTyCon tv r
t' r
_) = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t forall a. [a] -> [a] -> [a]
++ forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t'
tyClasses (RApp RTyCon
c [RType RTyCon tv r]
ts [RTProp RTyCon tv r]
_ r
_)
  | Just Class
cl <- TyCon -> Maybe Class
tyConClass_maybe forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
c
  = [(Class
cl, [RType RTyCon tv r]
ts)]
  | Bool
otherwise
  = []
tyClasses (RVar tv
_ r
_)      = []
tyClasses (RRTy [(Symbol, RType RTyCon tv r)]
_ r
_ Oblig
_ RType RTyCon tv r
t)  = forall tv r.
OkRT RTyCon tv r =>
RType RTyCon tv r -> [(Class, [RType RTyCon tv r])]
tyClasses RType RTyCon tv r
t
tyClasses (RHole r
_)       = []
tyClasses RType RTyCon tv r
t               = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing (String
"RefType.tyClasses cannot handle" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RType RTyCon tv r
t)


--------------------------------------------------------------------------------
-- TODO: Rewrite subsTyvars with Traversable
--------------------------------------------------------------------------------

subsTyVarsMeet
  :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsMeet :: forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsMeet        = forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> t (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVars Bool
True

subsTyVarsNoMeet
  :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsNoMeet :: forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsNoMeet      = forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> t (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVars Bool
False

subsTyVarNoMeet
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarNoMeet :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarNoMeet       = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVar Bool
False

subsTyVarMeet
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet         = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVar Bool
True

subsTyVarMeet'
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => (tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (tv
α, RType c tv r
t) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (tv
α, forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t, RType c tv r
t)

subsTyVars
  :: (Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> t (tv, RType c tv (), RType c tv r)
  -> RType c tv r
  -> RType c tv r
subsTyVars :: forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> t (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVars Bool
meet' t (tv, RType c tv (), RType c tv r)
ats RType c tv r
t = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVar Bool
meet')) RType c tv r
t t (tv, RType c tv (), RType c tv r)
ats

subsTyVar
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> (tv, RType c tv (), RType c tv r)
  -> RType c tv r
  -> RType c tv r
subsTyVar :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsTyVar Bool
meet'        = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
meet' forall a. HashSet a
S.empty

subsFree
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> S.HashSet tv
  -> (tv, RType c tv (), RType c tv r)
  -> RType c tv r
  -> RType c tv r
subsFree :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
α, RType c tv ()
τ,RType c tv r
_) (RAllP PVU c tv
π RType c tv r
t)
  = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) PVU c tv
π) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t)
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
a, RType c tv ()
τ, RType c tv r
_) (RAllT RTVar tv (RType c tv ())
α RType c tv r
t r
r)
  -- subt inside the type variable instantiates the kind of the variable
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
a, RType c tv ()
τ) RTVar tv (RType c tv ())
α) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m (forall tv s. RTVar tv s -> tv
ty_var_value RTVar tv (RType c tv ())
α forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` HashSet tv
s) (tv, RType c tv (), RType c tv r)
z RType c tv r
t) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
a, RType c tv ()
τ) r
r)
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
α, RType c tv ()
τ, RType c tv r
_) (RFun Symbol
x RFInfo
i RType c tv r
t RType c tv r
t' r
r)
  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t') (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r)
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
α, RType c tv ()
τ, RType c tv r
_) (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r)
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c' (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RTProp c tv r
-> RTProp c tv r
subsFreeRef Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp c tv r]
rs) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r)
    where z' :: (tv, RType c tv ())
z' = (tv
α, RType c tv ()
τ) -- UNIFY: why instantiating INSIDE parameters?
          c' :: c
c' = if tv
α forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet tv
s then c
c else forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, RType c tv ())
z' c
c
subsFree Bool
meet' HashSet tv
s (tv
α', RType c tv ()
τ, RType c tv r
t') (RVar tv
α r
r)
  | tv
α forall a. Eq a => a -> a -> Bool
== tv
α' Bool -> Bool -> Bool
&& Bool -> Bool
not (tv
α forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet tv
s)
  = if Bool
meet' then RType c tv r
t' forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r else RType c tv r
t'
  | Bool
otherwise
  = forall c tv r. tv -> r -> RType c tv r
RVar (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α', RType c tv ()
τ) tv
α) r
r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z (RAllE Symbol
x RType c tv r
t RType c tv r
t')
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t')
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z (REx Symbol
x RType c tv r
t RType c tv r
t')
  = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t')
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
α, RType c tv ()
τ, RType c tv r
_) (RAppTy RType c tv r
t RType c tv r
t' r
r)
  = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv -> RType c tv r -> RType c tv r -> r -> RType c tv r
subsFreeRAppTy Bool
m HashSet tv
s (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t) (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t') (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r)
subsFree Bool
_ HashSet tv
_ (tv, RType c tv (), RType c tv r)
_ t :: RType c tv r
t@(RExprArg Located Expr
_)
  = RType c tv r
t
subsFree Bool
m HashSet tv
s z :: (tv, RType c tv (), RType c tv r)
z@(tv
α, RType c tv ()
τ, RType c tv r
_) (RRTy [(Symbol, RType c tv r)]
e r
r Oblig
o RType c tv r
t)
  = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
e) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r) Oblig
o (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv, RType c tv (), RType c tv r)
z RType c tv r
t)
subsFree Bool
_ HashSet tv
_ (tv
α, RType c tv ()
τ, RType c tv r
_) (RHole r
r)
  = forall c tv r. r -> RType c tv r
RHole (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α, RType c tv ()
τ) r
r)

subsFrees
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> S.HashSet tv
  -> [(tv, RType c tv (), RType c tv r)]
  -> RType c tv r
  -> RType c tv r
subsFrees :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> [(tv, RType c tv (), RType c tv r)]
-> RType c tv r
-> RType c tv r
subsFrees Bool
m HashSet tv
s [(tv, RType c tv (), RType c tv r)]
zs RType c tv r
t = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s)) RType c tv r
t [(tv, RType c tv (), RType c tv r)]
zs

-- GHC INVARIANT: RApp is Type Application to something other than TYCon
subsFreeRAppTy
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()),
      FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> S.HashSet tv
  -> RType c tv r
  -> RType c tv r
  -> r
  -> RType c tv r
subsFreeRAppTy :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv -> RType c tv r -> RType c tv r -> r -> RType c tv r
subsFreeRAppTy Bool
m HashSet tv
s (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r) RType c tv r
t' r
r'
  = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> c
-> [RType c tv r]
-> [RTProp c tv r]
-> r
-> r
-> RType c tv r
mkRApp Bool
m HashSet tv
s c
c ([RType c tv r]
ts forall a. [a] -> [a] -> [a]
++ [RType c tv r
t']) [RTProp c tv r]
rs r
r r
r'
subsFreeRAppTy Bool
_ HashSet tv
_ RType c tv r
t RType c tv r
t' r
r'
  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy RType c tv r
t RType c tv r
t' r
r'


-- | @mkRApp@ is the refined variant of GHC's @mkTyConApp@ which ensures that
--    that applications of the "function" type constructor are normalized to
--    the special case @FunTy _@ representation. The extra `_rep1`, and `_rep2`
--    parameters come from the "levity polymorphism" changes in GHC 8.6 (?)
--    See [NOTE:Levity-Polymorphism]

mkRApp :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> S.HashSet tv
  -> c
  -> [RType c tv r]
  -> [RTProp c tv r]
  -> r
  -> r
  -> RType c tv r
mkRApp :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> c
-> [RType c tv r]
-> [RTProp c tv r]
-> r
-> r
-> RType c tv r
mkRApp Bool
m HashSet tv
s c
c [RType c tv r]
ts [RTProp c tv r]
rs r
r r
r'
  | forall c. TyConable c => c -> Bool
isFun c
c, [RType c tv r
_rep1, RType c tv r
_rep2, RType c tv r
t1, RType c tv r
t2] <- [RType c tv r]
ts
  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
dummySymbol RFInfo
defRFInfo RType c tv r
t1 RType c tv r
t2 (forall r. Reftable r => r -> r
refAppTyToFun r
r')
  | Bool
otherwise
  = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> [(tv, RType c tv (), RType c tv r)]
-> RType c tv r
-> RType c tv r
subsFrees Bool
m HashSet tv
s [(tv, RType c tv (), RType c tv r)]
zs (forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs (r
r forall r. Reftable r => r -> r -> r
`meet` r
r'))
  where
    zs :: [(tv, RType c tv (), RType c tv r)]
zs = [(tv
tv, forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t, RType c tv r
t) | (tv
tv, RType c tv r
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a v. FreeVar a v => a -> [v]
freeVars c
c) [RType c tv r]
ts]

{-| [NOTE:Levity-Polymorphism]

     Thanks to Joachim Brietner and Simon Peyton-Jones!
     With GHC's "levity polymorphism feature", see more here

         https://stackoverflow.com/questions/35318562/what-is-levity-polymorphism

     The function type constructor actually has type

        (->) :: forall (r1::RuntimeRep) (r2::RuntimeRep).  TYPE r1 -> TYPE r2 -> TYPE LiftedRep

     so we have to be careful to follow GHC's @mkTyConApp@

        https://hackage.haskell.org/package/ghc-8.6.4/docs/src/Type.html#mkTyConApp

     which normalizes applications of the `FunTyCon` constructor to use the special
     case `FunTy _` representation thus, so that we are not stuck with incompatible
     representations e.g.

        thing -> thing                                                  ... (using RFun)

     and

        (-> 'GHC.Types.LiftedRep 'GHC.Types.LiftedRep thing thing)      ... (using RApp)


     More details from Joachim Brietner:

     Now you might think that the function arrow has the following kind: `(->) :: * -> * -> *`.
     But that is not the full truth: You can have functions that accept or return things with
     different representations than just the usual lifted one.

     So the function arrow actually has kind `(->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> *`.
     And in `(-> 'GHC.Types.LiftedRep 'GHC.Types.LiftedRep thing thing)`  you see this spelled
     out explicitly. But it really is just `(thing -> thing)`, just printed with more low-level detail.

     Also see

       • https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#levity-polymorphism
       • and other links from https://stackoverflow.com/a/35320729/946226 (edited)
 -}

refAppTyToFun :: Reftable r => r -> r
refAppTyToFun :: forall r. Reftable r => r -> r
refAppTyToFun r
r
  | forall r. Reftable r => r -> Bool
isTauto r
r = r
r
  | Bool
otherwise = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType.refAppTyToFun"

subsFreeRef
  :: (Eq tv, Hashable tv, Reftable r, TyConable c,
      SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
      SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
      SubsTy tv (RType c tv ()) tv,
      SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ())))
  => Bool
  -> S.HashSet tv
  -> (tv, RType c tv (), RType c tv r)
  -> RTProp c tv r
  -> RTProp c tv r
subsFreeRef :: forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RTProp c tv r
-> RTProp c tv r
subsFreeRef Bool
_ HashSet tv
_ (tv
α', RType c tv ()
τ', RType c tv r
_) (RProp [(Symbol, RType c tv ())]
ss (RHole r
r))
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α', RType c tv ()
τ')) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) (forall c tv r. r -> RType c tv r
RHole r
r)
subsFreeRef Bool
m HashSet tv
s (tv
α', RType c tv ()
τ', RType c tv r
t')  (RProp [(Symbol, RType c tv ())]
ss RType c tv r
t)
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv
α', RType c tv ()
τ')) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) forall a b. (a -> b) -> a -> b
$ forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
Bool
-> HashSet tv
-> (tv, RType c tv (), RType c tv r)
-> RType c tv r
-> RType c tv r
subsFree Bool
m HashSet tv
s (tv
α', RType c tv ()
τ', forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall r. Reftable r => r -> r
top RType c tv r
t') RType c tv r
t


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

subts :: (SubsTy tv ty c) => [(tv, ty)] -> c -> c
subts :: forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts = forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt)

instance SubsTy RTyVar (RType RTyCon RTyVar ()) RTyVar where
  subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyVar -> RTyVar
subt (RTV TyVar
x, RType RTyCon RTyVar ()
t) (RTV TyVar
z) | TyVar -> Bool
isTyVar TyVar
z, TyVar -> Type
tyVarKind TyVar
z forall a. Eq a => a -> a -> Bool
== TyVar -> Type
TyVarTy TyVar
x
    = TyVar -> RTyVar
RTV (TyVar -> Type -> TyVar
setVarType TyVar
z forall a b. (a -> b) -> a -> b
$ forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RType RTyCon RTyVar ()
t)
  subt (RTyVar, RType RTyCon RTyVar ())
_ RTyVar
v
    = RTyVar
v

instance SubsTy RTyVar (RType RTyCon RTyVar ()) (RTVar RTyVar (RType RTyCon RTyVar ())) where
  -- NV TODO: update kind
  subt :: (RTyVar, RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subt (RTyVar, RType RTyCon RTyVar ())
su RTVar RTyVar (RType RTyCon RTyVar ())
rty = RTVar RTyVar (RType RTyCon RTyVar ())
rty { ty_var_value :: RTyVar
ty_var_value = forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (RTyVar, RType RTyCon RTyVar ())
su forall a b. (a -> b) -> a -> b
$ forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
rty }


instance SubsTy BTyVar (RType c BTyVar ()) BTyVar where
  subt :: (BTyVar, RType c BTyVar ()) -> BTyVar -> BTyVar
subt (BTyVar, RType c BTyVar ())
_ = forall a. a -> a
id

instance SubsTy BTyVar (RType c BTyVar ()) (RTVar BTyVar (RType c BTyVar ())) where
  subt :: (BTyVar, RType c BTyVar ())
-> RTVar BTyVar (RType c BTyVar ())
-> RTVar BTyVar (RType c BTyVar ())
subt (BTyVar, RType c BTyVar ())
_ = forall a. a -> a
id

instance SubsTy tv ty ()   where
  subt :: (tv, ty) -> () -> ()
subt (tv, ty)
_ = forall a. a -> a
id

instance SubsTy tv ty Symbol where
  subt :: (tv, ty) -> Symbol -> Symbol
subt (tv, ty)
_ = forall a. a -> a
id



instance (SubsTy tv ty Expr) => SubsTy tv ty Reft where
  subt :: (tv, ty) -> Reft -> Reft
subt (tv, ty)
su (Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> Reft
Reft (Symbol
x, forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e)

instance SubsTy Symbol Symbol (BRType r) where
  subt :: (Symbol, Symbol) -> BRType r -> BRType r
subt (Symbol
x,Symbol
y) (RVar BTyVar
v r
r)
    | Symbol -> BTyVar
BTV Symbol
x forall a. Eq a => a -> a -> Bool
== BTyVar
v = forall c tv r. tv -> r -> RType c tv r
RVar (Symbol -> BTyVar
BTV Symbol
y) r
r
    | Bool
otherwise  = forall c tv r. tv -> r -> RType c tv r
RVar BTyVar
v r
r
  subt (Symbol
x, Symbol
y) (RAllT (RTVar BTyVar
v RTVInfo (RType BTyCon BTyVar ())
i) BRType r
t r
r)
    | Symbol -> BTyVar
BTV Symbol
x forall a. Eq a => a -> a -> Bool
== BTyVar
v = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar BTyVar
v RTVInfo (RType BTyCon BTyVar ())
i) BRType r
t r
r
    | Bool
otherwise  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar BTyVar
v RTVInfo (RType BTyCon BTyVar ())
i) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol
x,Symbol
y) BRType r
t) r
r
  subt (Symbol, Symbol)
su (RFun Symbol
x RFInfo
i BRType r
t1 BRType r
t2 r
r)  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t2) r
r
  subt (Symbol, Symbol)
su (RAllP PVU BTyCon BTyVar
p BRType r
t)       = forall c tv r. PVar (RType c tv ()) -> RType c tv r -> RType c tv r
RAllP PVU BTyCon BTyVar
p (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t)
  subt (Symbol, Symbol)
su (RApp BTyCon
c [BRType r]
ts [RTProp BTyCon BTyVar r]
ps r
r)  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp BTyCon
c (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BRType r]
ts) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp BTyCon BTyVar r]
ps) r
r
  subt (Symbol, Symbol)
su (RAllE Symbol
x BRType r
t1 BRType r
t2)   = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t2)
  subt (Symbol, Symbol)
su (REx Symbol
x BRType r
t1 BRType r
t2)     = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t2)
  subt (Symbol, Symbol)
_  (RExprArg Located Expr
e)      = forall c tv r. Located Expr -> RType c tv r
RExprArg Located Expr
e
  subt (Symbol, Symbol)
su (RAppTy BRType r
t1 BRType r
t2 r
r)  = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t2) r
r
  subt (Symbol, Symbol)
su (RRTy [(Symbol, BRType r)]
e r
r Oblig
o BRType r
t)    = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol
x, forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
p) | (Symbol
x,BRType r
p) <- [(Symbol, BRType r)]
e] r
r Oblig
o (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su BRType r
t)
  subt (Symbol, Symbol)
_ (RHole r
r)          = forall c tv r. r -> RType c tv r
RHole r
r

instance SubsTy Symbol Symbol (RTProp BTyCon BTyVar r) where
  subt :: (Symbol, Symbol)
-> RTProp BTyCon BTyVar r -> RTProp BTyCon BTyVar r
subt (Symbol, Symbol)
su (RProp [(Symbol, RType BTyCon BTyVar ())]
e RType BTyCon BTyVar r
t) =  forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol
x, forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su RType BTyCon BTyVar ()
xt) | (Symbol
x,RType BTyCon BTyVar ()
xt) <- [(Symbol, RType BTyCon BTyVar ())]
e] (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (Symbol, Symbol)
su RType BTyCon BTyVar r
t)



instance (SubsTy tv ty Sort) => SubsTy tv ty Expr where
  subt :: (tv, ty) -> Expr -> Expr
subt (tv, ty)
su (ELam (Symbol
x, Sort
s) Expr
e) = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Sort
s) forall a b. (a -> b) -> a -> b
$ forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e
  subt (tv, ty)
su (EApp Expr
e1 Expr
e2)    = Expr -> Expr -> Expr
EApp (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (ENeg Expr
e)        = Expr -> Expr
ENeg (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e)
  subt (tv, ty)
su (PNot Expr
e)        = Expr -> Expr
PNot (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e)
  subt (tv, ty)
su (EBin Bop
b Expr
e1 Expr
e2)  = Bop -> Expr -> Expr -> Expr
EBin Bop
b (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (EIte Expr
e Expr
e1 Expr
e2)  = Expr -> Expr -> Expr -> Expr
EIte (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (ECst Expr
e Sort
s)      = Expr -> Sort -> Expr
ECst (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Sort
s)
  subt (tv, ty)
su (ETApp Expr
e Sort
s)     = Expr -> Sort -> Expr
ETApp (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Sort
s)
  subt (tv, ty)
su (ETAbs Expr
e Symbol
x)     = Expr -> Symbol -> Expr
ETAbs (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e) Symbol
x
  subt (tv, ty)
su (PAnd [Expr]
es)       = [Expr] -> Expr
PAnd (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  subt (tv, ty)
su (POr  [Expr]
es)       = [Expr] -> Expr
POr  (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  subt (tv, ty)
su (PImp Expr
e1 Expr
e2)    = Expr -> Expr -> Expr
PImp (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (PIff Expr
e1 Expr
e2)    = Expr -> Expr -> Expr
PIff (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (PAtom Brel
b Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
PAtom Brel
b (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e1) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e2)
  subt (tv, ty)
su (PAll [(Symbol, Sort)]
xes Expr
e)    = [(Symbol, Sort)] -> Expr -> Expr
PAll (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xes) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e)
  subt (tv, ty)
su (PExist [(Symbol, Sort)]
xes Expr
e)  = [(Symbol, Sort)] -> Expr -> Expr
PExist (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xes) (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su Expr
e)
  subt (tv, ty)
_ Expr
e                = Expr
e

instance (SubsTy tv ty a, SubsTy tv ty b) => SubsTy tv ty (a, b) where
  subt :: (tv, ty) -> (a, b) -> (a, b)
subt (tv, ty)
su (a
x, b
y) = (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su a
x, forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su b
y)

instance SubsTy BTyVar (RType BTyCon BTyVar ()) Sort where
  subt :: (BTyVar, RType BTyCon BTyVar ()) -> Sort -> Sort
subt (BTyVar
v, RVar BTyVar
α ()
_) (FObj Symbol
s)
    | forall a. Symbolic a => a -> Symbol
symbol BTyVar
v forall a. Eq a => a -> a -> Bool
== Symbol
s = Symbol -> Sort
FObj forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol BTyVar
α
    | Bool
otherwise     = Symbol -> Sort
FObj Symbol
s
  subt (BTyVar, RType BTyCon BTyVar ())
_ Sort
s          = Sort
s


instance SubsTy Symbol RSort Sort where
  subt :: (Symbol, RType RTyCon RTyVar ()) -> Sort -> Sort
subt (Symbol
v, RVar RTyVar
α ()
_) (FObj Symbol
s)
    | forall a. Symbolic a => a -> Symbol
symbol Symbol
v forall a. Eq a => a -> a -> Bool
== Symbol
s = Symbol -> Sort
FObj forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol {- rTyVarSymbol -} RTyVar
α
    | Bool
otherwise     = Symbol -> Sort
FObj Symbol
s
  subt (Symbol, RType RTyCon RTyVar ())
_ Sort
s          = Sort
s


instance SubsTy RTyVar RSort Sort where
  subt :: (RTyVar, RType RTyCon RTyVar ()) -> Sort -> Sort
subt (RTyVar
v, RType RTyCon RTyVar ()
sv) (FObj Symbol
s)
    | forall a. Symbolic a => a -> Symbol
symbol RTyVar
v forall a. Eq a => a -> a -> Bool
== Symbol
s = TCEmb TyCon -> Type -> Sort
typeSort forall a. Monoid a => a
mempty (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
True RType RTyCon RTyVar ()
sv)
    | Bool
otherwise     = Symbol -> Sort
FObj Symbol
s
  subt (RTyVar, RType RTyCon RTyVar ())
_ Sort
s          = Sort
s

instance (SubsTy tv ty ty) => SubsTy tv ty (PVKind ty) where
  subt :: (tv, ty) -> PVKind ty -> PVKind ty
subt (tv, ty)
su (PVProp ty
t) = forall t. t -> PVKind t
PVProp (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su ty
t)
  subt (tv, ty)
_   PVKind ty
PVHProp   = forall t. PVKind t
PVHProp

instance (SubsTy tv ty ty) => SubsTy tv ty (PVar ty) where
  subt :: (tv, ty) -> PVar ty -> PVar ty
subt (tv, ty)
su (PV Symbol
n PVKind ty
pvk Symbol
v [(ty, Symbol, Expr)]
xts) = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
n (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su PVKind ty
pvk) Symbol
v [(forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su ty
t, Symbol
x, Expr
y) | (ty
t,Symbol
x,Expr
y) <- [(ty, Symbol, Expr)]
xts]

instance SubsTy RTyVar RSort RTyCon where
   subt :: (RTyVar, RType RTyCon RTyVar ()) -> RTyCon -> RTyCon
subt (RTyVar, RType RTyCon RTyVar ())
z RTyCon
c = TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon TyCon
tc [RPVar]
ps' TyConInfo
i
     where
       tc :: TyCon
tc   = RTyCon -> TyCon
rtc_tc RTyCon
c
       ps' :: [RPVar]
ps'  = forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (RTyVar, RType RTyCon RTyVar ())
z forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTyCon -> [RPVar]
rTyConPVs RTyCon
c
       i :: TyConInfo
i    = RTyCon -> TyConInfo
rtc_info RTyCon
c

-- NOTE: This DOES NOT substitute at the binders
instance SubsTy RTyVar RSort PrType where
  subt :: (RTyVar, RType RTyCon RTyVar ()) -> PrType -> PrType
subt (RTyVar
α, RType RTyCon RTyVar ()
τ) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (RTyVar
α, RType RTyCon RTyVar ()
τ, forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
τ)

instance SubsTy RTyVar RSort SpecType where
  subt :: (RTyVar, RType RTyCon RTyVar ()) -> SpecType -> SpecType
subt (RTyVar
α, RType RTyCon RTyVar ()
τ) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (RTyVar
α, RType RTyCon RTyVar ()
τ, forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
τ)

instance SubsTy TyVar Type SpecType where
  subt :: (TyVar, Type) -> SpecType -> SpecType
subt (TyVar
α, Type
τ) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (TyVar -> RTyVar
RTV TyVar
α, forall r. Monoid r => Type -> RRType r
ofType Type
τ, forall r. Monoid r => Type -> RRType r
ofType Type
τ)

instance SubsTy RTyVar RTyVar SpecType where
  subt :: (RTyVar, RTyVar) -> SpecType -> SpecType
subt (RTyVar
α, RTyVar
a) = forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (RTyVar
α, forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a () :: RSort)


instance SubsTy RTyVar RSort RSort where
  subt :: (RTyVar, RType RTyCon RTyVar ())
-> RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
subt (RTyVar
α, RType RTyCon RTyVar ()
τ) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (RTyVar
α, RType RTyCon RTyVar ()
τ, forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
τ)

instance SubsTy tv RSort Predicate where
  subt :: (tv, RType RTyCon RTyVar ()) -> Predicate -> Predicate
subt (tv, RType RTyCon RTyVar ())
_ = forall a. a -> a
id -- NV TODO

instance (SubsTy tv ty r) => SubsTy tv ty (UReft r) where
  subt :: (tv, ty) -> UReft r -> UReft r
subt (tv, ty)
su UReft r
r = UReft r
r {ur_reft :: r
ur_reft = forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
su forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft UReft r
r}

-- Here the "String" is a Bare-TyCon. TODO: wrap in newtype
instance SubsTy BTyVar BSort BTyCon where
  subt :: (BTyVar, RType BTyCon BTyVar ()) -> BTyCon -> BTyCon
subt (BTyVar, RType BTyCon BTyVar ())
_ BTyCon
t = BTyCon
t

instance SubsTy BTyVar BSort BSort where
  subt :: (BTyVar, RType BTyCon BTyVar ())
-> RType BTyCon BTyVar () -> RType BTyCon BTyVar ()
subt (BTyVar
α, RType BTyCon BTyVar ()
τ) = forall tv r c.
(Eq tv, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
(tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet (BTyVar
α, RType BTyCon BTyVar ()
τ, forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType BTyCon BTyVar ()
τ)

instance (SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))  where
  subt :: (tv, ty) -> RTProp c tv (UReft r) -> RTProp c tv (UReft r)
subt (tv, ty)
m (RProp [(Symbol, RType c tv ())]
ss (RHole UReft r
p)) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) forall a b. (a -> b) -> a -> b
$ forall c tv r. r -> RType c tv r
RHole forall a b. (a -> b) -> a -> b
$ forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
m UReft r
p
  subt (tv, ty)
m (RProp [(Symbol, RType c tv ())]
ss RType c tv (UReft r)
t) = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt (tv, ty)
m) RType c tv (UReft r)
t

subvUReft     :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
subvUReft :: (UsedPVar -> UsedPVar) -> UReft Reft -> UReft Reft
subvUReft UsedPVar -> UsedPVar
f (MkUReft Reft
r Predicate
p) = forall r. r -> Predicate -> UReft r
MkUReft Reft
r ((UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvPredicate UsedPVar -> UsedPVar
f Predicate
p)

subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvPredicate :: (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvPredicate UsedPVar -> UsedPVar
f (Pr [UsedPVar]
pvs) = [UsedPVar] -> Predicate
Pr (UsedPVar -> UsedPVar
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
pvs)

--------------------------------------------------------------------------------
ofType :: Monoid r => Type -> RRType r
--------------------------------------------------------------------------------
ofType :: forall r. Monoid r => Type -> RRType r
ofType      = forall r c tv. Monoid r => TyConv c tv r -> Type -> RType c tv r
ofType_ forall a b. (a -> b) -> a -> b
$ TyConv
  { tcFVar :: TyVar -> RType RTyCon RTyVar r
tcFVar  = forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar
  , tcFTVar :: TyVar -> RTVar RTyVar (RType RTyCon RTyVar ())
tcFTVar = forall r. Monoid r => TyVar -> RTVar RTyVar (RRType r)
rTVar
  , tcFApp :: TyCon -> [RType RTyCon RTyVar r] -> RType RTyCon RTyVar r
tcFApp  = \TyCon
c [RType RTyCon RTyVar r]
ts -> forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [RType RTyCon RTyVar r]
ts [] forall a. Monoid a => a
mempty
  , tcFLit :: TyLit -> RType RTyCon RTyVar r
tcFLit  = forall r c tv p.
Monoid r =>
(TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r)
-> TyLit -> RType c tv r
ofLitType forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp
  }

--------------------------------------------------------------------------------
bareOfType :: Monoid r => Type -> BRType r
--------------------------------------------------------------------------------
bareOfType :: forall r. Monoid r => Type -> BRType r
bareOfType  = forall r c tv. Monoid r => TyConv c tv r -> Type -> RType c tv r
ofType_ forall a b. (a -> b) -> a -> b
$ TyConv
  { tcFVar :: TyVar -> RType BTyCon BTyVar r
tcFVar  = (forall c tv r. tv -> r -> RType c tv r
`RVar` forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> BTyVar
BTV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol
  , tcFTVar :: TyVar -> RTVar BTyVar (RType BTyCon BTyVar ())
tcFTVar = forall r. Monoid r => TyVar -> RTVar BTyVar (BRType r)
bTVar
  , tcFApp :: TyCon -> [RType BTyCon BTyVar r] -> RType BTyCon BTyVar r
tcFApp  = \TyCon
c [RType BTyCon BTyVar r]
ts -> forall r. TyCon -> [BRType r] -> [BRProp r] -> r -> BRType r
bApp TyCon
c [RType BTyCon BTyVar r]
ts [] forall a. Monoid a => a
mempty
  , tcFLit :: TyLit -> RType BTyCon BTyVar r
tcFLit  = forall r c tv p.
Monoid r =>
(TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r)
-> TyLit -> RType c tv r
ofLitType forall r. TyCon -> [BRType r] -> [BRProp r] -> r -> BRType r
bApp
  }

--------------------------------------------------------------------------------
ofType_ :: Monoid r => TyConv c tv r -> Type -> RType c tv r
--------------------------------------------------------------------------------
ofType_ :: forall r c tv. Monoid r => TyConv c tv r -> Type -> RType c tv r
ofType_ TyConv c tv r
tx = Type -> RType c tv r
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
expandTypeSynonyms
  where
    go :: Type -> RType c tv r
go (TyVarTy TyVar
α)
      = forall c tv r. TyConv c tv r -> TyVar -> RType c tv r
tcFVar TyConv c tv r
tx TyVar
α
    go (FunTy AnonArgFlag
_ Type
_ Type
τ Type
τ')
      = forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun Symbol
dummySymbol (Type -> RType c tv r
go Type
τ) (Type -> RType c tv r
go Type
τ')
    go (ForAllTy (Bndr TyVar
α ArgFlag
_) Type
τ)
      = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall c tv r. TyConv c tv r -> TyVar -> RTVar tv (RType c tv ())
tcFTVar TyConv c tv r
tx TyVar
α) (Type -> RType c tv r
go Type
τ) forall a. Monoid a => a
mempty
    go (TyConApp TyCon
c [Type]
τs)
      | Just ([TyVar]
αs, Type
τ) <- TyCon -> Maybe ([TyVar], Type)
Ghc.synTyConDefn_maybe TyCon
c
      = Type -> RType c tv r
go (HasCallStack => [TyVar] -> [Type] -> Type -> Type
substTyWith [TyVar]
αs [Type]
τs Type
τ)
      | Bool
otherwise
      = forall c tv r.
TyConv c tv r -> TyCon -> [RType c tv r] -> RType c tv r
tcFApp TyConv c tv r
tx TyCon
c (Type -> RType c tv r
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
τs) -- [] mempty
    go (AppTy Type
t1 Type
t2)
      = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (Type -> RType c tv r
go Type
t1) (forall r c tv. Monoid r => TyConv c tv r -> Type -> RType c tv r
ofType_ TyConv c tv r
tx Type
t2) forall a. Monoid a => a
mempty
    go (LitTy TyLit
x)
      = forall c tv r. TyConv c tv r -> TyLit -> RType c tv r
tcFLit TyConv c tv r
tx TyLit
x
    go (CastTy Type
t KindCoercion
_)
      = Type -> RType c tv r
go Type
t
    go (CoercionTy KindCoercion
_)
      = forall a. HasCallStack => String -> a
errorstar String
"Coercion is currently not supported"

ofLitType :: (Monoid r) => (TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r) -> TyLit -> RType c tv r
ofLitType :: forall r c tv p.
Monoid r =>
(TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r)
-> TyLit -> RType c tv r
ofLitType TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r
rF (NumTyLit Integer
_)  = TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r
rF TyCon
intTyCon [] [] forall a. Monoid a => a
mempty
ofLitType TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r
rF t :: TyLit
t@(StrTyLit FastString
_)
  | TyLit
t forall a. Eq a => a -> a -> Bool
== TyLit
holeLit           = forall c tv r. r -> RType c tv r
RHole forall a. Monoid a => a
mempty
  | Bool
otherwise              = TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r
rF TyCon
listTyCon [TyCon -> [RType c tv r] -> [p] -> r -> RType c tv r
rF TyCon
charTyCon [] [] forall a. Monoid a => a
mempty] [] forall a. Monoid a => a
mempty

holeLit :: TyLit
holeLit :: TyLit
holeLit = FastString -> TyLit
StrTyLit FastString
"$LH_RHOLE"

data TyConv c tv r = TyConv
  { forall c tv r. TyConv c tv r -> TyVar -> RType c tv r
tcFVar  :: TyVar -> RType c tv r
  , forall c tv r. TyConv c tv r -> TyVar -> RTVar tv (RType c tv ())
tcFTVar :: TyVar -> RTVar tv (RType c tv ())
  , forall c tv r.
TyConv c tv r -> TyCon -> [RType c tv r] -> RType c tv r
tcFApp  :: TyCon -> [RType c tv r] -> RType c tv r
  , forall c tv r. TyConv c tv r -> TyLit -> RType c tv r
tcFLit  :: TyLit -> RType c tv r
  }

--------------------------------------------------------------------------------
-- | Converting to Fixpoint ----------------------------------------------------
--------------------------------------------------------------------------------


instance Expression Var where
  expr :: TyVar -> Expr
expr   = forall a. Symbolic a => a -> Expr
eVar

-- TODO: turn this into a map lookup?
dataConReft ::  DataCon -> [Symbol] -> Reft
dataConReft :: DataCon -> [Symbol] -> Reft
dataConReft DataCon
c []
  | DataCon
c forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon
  = forall a. Predicate a => a -> Reft
predReft forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Expr
eProp Symbol
vv_
  | DataCon
c forall a. Eq a => a -> a -> Bool
== DataCon
falseDataCon
  = forall a. Predicate a => a -> Reft
predReft forall a b. (a -> b) -> a -> b
$ Expr -> Expr
PNot forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Expr
eProp Symbol
vv_

dataConReft DataCon
c [Symbol
x]
  | DataCon
c forall a. Eq a => a -> a -> Bool
== DataCon
intDataCon
  = forall a. Symbolic a => a -> Reft
symbolReft Symbol
x -- OLD (vv_, [RConc (PAtom Eq (EVar vv_) (EVar x))])
dataConReft DataCon
c [Symbol]
_
  | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ DataCon -> Bool
isBaseDataCon DataCon
c
  = forall a. Monoid a => a
mempty
dataConReft DataCon
c [Symbol]
xs
  = forall a. Expression a => a -> Reft
exprReft Expr
dcValue -- OLD Reft (vv_, [RConc (PAtom Eq (EVar vv_) dcValue)])
  where
    dcValue :: Expr
dcValue
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol]
xs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [TyVar]
dataConUnivTyVars DataCon
c)
      = Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol DataCon
c
      | Bool
otherwise
      = LocSymbol -> [Expr] -> Expr
mkEApp (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
symbol DataCon
c) (forall a. Symbolic a => a -> Expr
eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)

isBaseDataCon :: DataCon -> Bool
isBaseDataCon :: DataCon -> Bool
isBaseDataCon DataCon
c = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ Type -> Bool
isBaseTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
irrelevantMult (DataCon -> [Scaled Type]
dataConOrigArgTys DataCon
c forall a. [a] -> [a] -> [a]
++ DataCon -> [Scaled Type]
dataConRepArgTys DataCon
c)

isBaseTy :: Type -> Bool
isBaseTy :: Type -> Bool
isBaseTy (TyVarTy TyVar
_)      = Bool
True
isBaseTy (AppTy Type
_ Type
_)      = Bool
False
isBaseTy (TyConApp TyCon
_ [Type]
ts)  = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ Type -> Bool
isBaseTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts
isBaseTy FunTy{}          = Bool
False
isBaseTy (ForAllTy VarBndr TyVar ArgFlag
_ Type
_)   = Bool
False
isBaseTy (LitTy TyLit
_)        = Bool
True
isBaseTy (CastTy Type
_ KindCoercion
_)     = Bool
False
isBaseTy (CoercionTy KindCoercion
_)   = Bool
False


dataConMsReft :: Reftable r => RType c tv r -> [Symbol] -> Reft
dataConMsReft :: forall r c tv. Reftable r => RType c tv r -> [Symbol] -> Reft
dataConMsReft RType c tv r
ty [Symbol]
ys  = forall a. Subable a => Subst -> a -> a
subst Subst
su (forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft (forall t t1 t2. RType t t1 t2 -> RType t t1 t2
ignoreOblig forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep c tv r
trep))
  where
    trep :: RTypeRep c tv r
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType c tv r
ty
    xs :: [Symbol]
xs   = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep c tv r
trep
    ts :: [RType c tv r]
ts   = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep c tv r
trep
    su :: Subst
su   = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ [(Symbol
x, Symbol -> Expr
EVar Symbol
y) | ((Symbol
x, RType c tv r
_), Symbol
y) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [RType c tv r]
ts) [Symbol]
ys]

--------------------------------------------------------------------------------
-- | Embedding RefTypes --------------------------------------------------------
--------------------------------------------------------------------------------

type ToTypeable r = (Reftable r, PPrint r, SubsTy RTyVar (RRType ()) r, Reftable (RTProp RTyCon RTyVar r))

-- TODO: remove toType, generalize typeSort
-- YL: really should take a type-level Bool
toType  :: (ToTypeable r) => Bool -> RRType r -> Type
toType :: forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo (RFun Symbol
_ RFInfo{permitTC :: RFInfo -> Maybe Bool
permitTC = Maybe Bool
permitTC} t :: RRType r
t@(RApp RTyCon
c [RRType r]
_ [RTProp RTyCon RTyVar r]
_ r
_) RRType r
t' r
_)
  | Bool
useRFInfo Bool -> Bool -> Bool
&& RTyCon -> Bool
isErasable RTyCon
c = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t'
  | Bool
otherwise
  = AnonArgFlag -> Type -> Type -> Type -> Type
FunTy AnonArgFlag
VisArg Type
Many (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t) (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t')
  where isErasable :: RTyCon -> Bool
isErasable = if Maybe Bool
permitTC forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Bool
True then forall c. TyConable c => c -> Bool
isEmbeddedDict else forall c. TyConable c => c -> Bool
isClass
toType Bool
useRFInfo (RFun Symbol
_ RFInfo
_ RRType r
t RRType r
t' r
_)
  = AnonArgFlag -> Type -> Type -> Type -> Type
FunTy AnonArgFlag
VisArg Type
Many (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t) (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t')
toType Bool
useRFInfo (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a RRType r
t r
_) | RTV TyVar
α <- forall tv s. RTVar tv s -> tv
ty_var_value RTVar RTyVar (RType RTyCon RTyVar ())
a
  = VarBndr TyVar ArgFlag -> Type -> Type
ForAllTy (forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
α ArgFlag
Required) (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t)
toType Bool
useRFInfo (RAllP RPVar
_ RRType r
t)
  = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t
toType Bool
_ (RVar (RTV TyVar
α) r
_)
  = TyVar -> Type
TyVarTy TyVar
α
toType Bool
useRFInfo (RApp RTyCon{rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
c} [RRType r]
ts [RTProp RTyCon RTyVar r]
_ r
_)
  = TyCon -> [Type] -> Type
TyConApp TyCon
c (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter forall {c} {tv} {r}. RType c tv r -> Bool
notExprArg [RRType r]
ts)
  where
    notExprArg :: RType c tv r -> Bool
notExprArg (RExprArg Located Expr
_) = Bool
False
    notExprArg RType c tv r
_            = Bool
True
toType Bool
useRFInfo (RAllE Symbol
_ RRType r
_ RRType r
t)
  = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t
toType Bool
useRFInfo (REx Symbol
_ RRType r
_ RRType r
t)
  = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t
toType Bool
useRFInfo (RAppTy RRType r
t (RExprArg Located Expr
_) r
_)
  = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t
toType Bool
useRFInfo (RAppTy RRType r
t RRType r
t' r
_)
  = Type -> Type -> Type
AppTy (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t) (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t')
toType Bool
_ t :: RRType r
t@(RExprArg Located Expr
_)
  = forall a. Maybe SrcSpan -> String -> a
impossible forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"CANNOT HAPPEN: RefType.toType called with: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RRType r
t
toType Bool
useRFInfo (RRTy [(Symbol, RRType r)]
_ r
_ Oblig
_ RRType r
t)
  = forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
useRFInfo RRType r
t
toType Bool
_ (RHole r
_)
  = TyLit -> Type
LitTy TyLit
holeLit
-- toType t
--  = {- impossible Nothing -} Prelude.error $ "RefType.toType cannot handle: " ++ show t

{- | [NOTE:Hole-Lit]

We use `toType` to convert RType to GHC.Type to expand any GHC
related type-aliases, e.g. in Bare.Resolve.expandRTypeSynonyms.
If the RType has a RHole then what to do?

We, encode `RHole` as `LitTy "LH_HOLE"` -- which is a bit of
a *hack*. The only saving grace is it is used *temporarily*
and then swiftly turned back into an `RHole` via `ofType`
(after GHC has done its business of expansion).

Of course, we hope this doesn't break any GHC invariants!
See issue #1476 and #1477

The other option is to *not* use `toType` on things that have
holes in them, but this seems worse, e.g. because you may define
a plain GHC alias like:

    type ToNat a = a -> Nat

and then you might write refinement types like:

    {-@ foo :: ToNat {v:_ | 0 <= v} @-}

and we'd want to expand the above to

    {-@ foo :: {v:_ | 0 <= v} -> Nat @-}

and then resolve the hole using the (GHC) type of `foo`.

-}

--------------------------------------------------------------------------------
-- | Annotations and Solutions -------------------------------------------------
--------------------------------------------------------------------------------

rTypeSortedReft ::  (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
                => TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb RRType r
t = Sort -> Reft -> SortedReft
RR (forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
emb RRType r
t) (forall r c tv. Reftable r => RType c tv r -> Reft
rTypeReft RRType r
t)

rTypeSort     ::  (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
              => TCEmb TyCon -> RRType r -> Sort
rTypeSort :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
True

--------------------------------------------------------------------------------
applySolution :: (Functor f) => FixSolution -> f SpecType -> f SpecType
--------------------------------------------------------------------------------
applySolution :: forall (f :: * -> *).
Functor f =>
FixSolution -> f SpecType -> f SpecType
applySolution = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> UReft Reft -> UReft Reft
mapReft' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Visitable t => FixSolution -> t -> t
appSolRefa
  where
    mapReft' :: (Expr -> Expr) -> UReft Reft -> UReft Reft
mapReft' Expr -> Expr
f (MkUReft (Reft (Symbol
x, Expr
z)) Predicate
p) = forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr -> Expr
f Expr
z)) Predicate
p

appSolRefa :: Visitable t
           => M.HashMap KVar Expr -> t -> t
appSolRefa :: forall t. Visitable t => FixSolution -> t -> t
appSolRefa FixSolution
s t
p = forall t. Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars KVar -> Maybe Expr
f t
p
  where
    f :: KVar -> Maybe Expr
f KVar
k        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Expr
PTop KVar
k FixSolution
s

--------------------------------------------------------------------------------
-- shiftVV :: Int -- SpecType -> Symbol -> SpecType
shiftVV :: (TyConable c, F.Reftable (f Reft), Functor f)
        => RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
--------------------------------------------------------------------------------
shiftVV :: forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV t :: RType c tv (f Reft)
t@(RApp c
_ [RType c tv (f Reft)]
ts [RTProp c tv (f Reft)]
rs f Reft
r) Symbol
vv'
  = RType c tv (f Reft)
t { rt_args :: [RType c tv (f Reft)]
rt_args  = forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 [RType c tv (f Reft)]
ts (forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv (f Reft)
t, Symbol -> Expr
EVar Symbol
vv') }
      { rt_pargs :: [RTProp c tv (f Reft)]
rt_pargs = forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 [RTProp c tv (f Reft)]
rs (forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv (f Reft)
t, Symbol -> Expr
EVar Symbol
vv') }
      { rt_reft :: f Reft
rt_reft  = (Reft -> Symbol -> Reft
`F.shiftVV` Symbol
vv') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Reft
r }

shiftVV t :: RType c tv (f Reft)
t@(RFun Symbol
_ RFInfo
_ RType c tv (f Reft)
_ RType c tv (f Reft)
_ f Reft
r) Symbol
vv'
  = RType c tv (f Reft)
t { rt_reft :: f Reft
rt_reft = (Reft -> Symbol -> Reft
`F.shiftVV` Symbol
vv') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Reft
r }

shiftVV t :: RType c tv (f Reft)
t@(RAppTy RType c tv (f Reft)
_ RType c tv (f Reft)
_ f Reft
r) Symbol
vv'
  = RType c tv (f Reft)
t { rt_reft :: f Reft
rt_reft = (Reft -> Symbol -> Reft
`F.shiftVV` Symbol
vv') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Reft
r }

shiftVV t :: RType c tv (f Reft)
t@(RVar tv
_ f Reft
r) Symbol
vv'
  = RType c tv (f Reft)
t { rt_reft :: f Reft
rt_reft = (Reft -> Symbol -> Reft
`F.shiftVV` Symbol
vv') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Reft
r }

shiftVV RType c tv (f Reft)
t Symbol
_
  = RType c tv (f Reft)
t -- errorstar $ "shiftVV: cannot handle " ++ showpp t


--------------------------------------------------------------------------------
-- |Auxiliary Stuff Used Elsewhere ---------------------------------------------
--------------------------------------------------------------------------------

-- MOVE TO TYPES
instance (Show tv, Show ty) => Show (RTAlias tv ty) where
  show :: RTAlias tv ty -> String
show (RTA Symbol
n [tv]
as [Symbol]
xs ty
t) =
    forall r. PrintfType r => String -> r
printf String
"type %s %s %s = %s" (Symbol -> String
symbolString Symbol
n)
      ([String] -> String
unwords (forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [tv]
as))
      ([String] -> String
unwords (forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
      (forall a. Show a => a -> String
show ty
t)

--------------------------------------------------------------------------------
-- | From Old Fixpoint ---------------------------------------------------------
--------------------------------------------------------------------------------
typeSort :: TCEmb TyCon -> Type -> Sort
typeSort :: TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce = Type -> Sort
go
  where
    go :: Type -> Sort
    go :: Type -> Sort
go t :: Type
t@FunTy{}        = TCEmb TyCon -> Type -> Sort
typeSortFun TCEmb TyCon
tce Type
t
    go τ :: Type
τ@(ForAllTy VarBndr TyVar ArgFlag
_ Type
_) = TCEmb TyCon -> Type -> Sort
typeSortForAll TCEmb TyCon
tce Type
τ
    -- go (TyConApp c τs)  = fApp (tyConFTyCon tce c) (go <$> τs)
    go (TyConApp TyCon
c [Type]
τs)
      | TyCon -> Bool
isNewTyCon TyCon
c
      , Bool -> Bool
not (TyCon -> Bool
isRecursivenewTyCon TyCon
c)
      = Type -> Sort
go (TyCon -> [Type] -> Type
Ghc.newTyConInstRhs TyCon
c [Type]
τs)
      | Bool
otherwise
      = TCEmb TyCon -> TyCon -> [Sort] -> Sort
tyConFTyCon TCEmb TyCon
tce TyCon
c (Type -> Sort
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
τs)
    go (AppTy Type
t1 Type
t2)    = Sort -> [Sort] -> Sort
fApp (Type -> Sort
go Type
t1) [Type -> Sort
go Type
t2]
    go (TyVarTy TyVar
tv)     = TyVar -> Sort
tyVarSort TyVar
tv
    go (CastTy Type
t KindCoercion
_)     = Type -> Sort
go Type
t
    go Type
τ                = Symbol -> Sort
FObj (Type -> Symbol
typeUniqueSymbol Type
τ)

tyConFTyCon :: TCEmb TyCon -> TyCon -> [Sort] -> Sort
tyConFTyCon :: TCEmb TyCon -> TyCon -> [Sort] -> Sort
tyConFTyCon TCEmb TyCon
tce TyCon
c [Sort]
ts = case forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
tceLookup TyCon
c TCEmb TyCon
tce of
                         Just (Sort
t, TCArgs
WithArgs) -> Sort
t
                         Just (Sort
t, TCArgs
NoArgs)   -> Sort -> [Sort] -> Sort
fApp Sort
t [Sort]
ts
                         Maybe (Sort, TCArgs)
Nothing            -> Sort -> [Sort] -> Sort
fApp (FTycon -> Sort
fTyconSort FTycon
niTc) [Sort]
ts
  where
    niTc :: FTycon
niTc             = LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ TyCon -> Symbol
tyConName TyCon
c) (forall c. TyConable c => c -> Bool
isNumCls TyCon
c) (forall c. TyConable c => c -> Bool
isFracCls TyCon
c)
    -- oldRes           = F.notracepp _msg $ M.lookupDefault def c tce
    -- _msg             = "tyConFTyCon c = " ++ show c ++ "default " ++ show (def, Ghc.isFamInstTyCon c)

tyVarSort :: TyVar -> Sort
tyVarSort :: TyVar -> Sort
tyVarSort = Symbol -> Sort
FObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol

typeUniqueSymbol :: Type -> Symbol
typeUniqueSymbol :: Type -> Symbol
typeUniqueSymbol = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> String
GM.typeUniqueString

typeSortForAll :: TCEmb TyCon -> Type -> Sort
typeSortForAll :: TCEmb TyCon -> Type -> Sort
typeSortForAll TCEmb TyCon
tce Type
τ  = forall a. PPrint a => String -> a -> a
F.notracepp (String
"typeSortForall " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Type
τ) forall a b. (a -> b) -> a -> b
$ Sort -> Sort
genSort Sort
sbody
  where
    sbody :: Sort
sbody             = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce Type
tbody
    genSort :: Sort -> Sort
genSort Sort
t         = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sort -> Sort
FAbs) (SortSubst -> Sort -> Sort
sortSubst SortSubst
su Sort
t) [Int
i..Int
nforall a. Num a => a -> a -> a
+Int
iforall a. Num a => a -> a -> a
-Int
1]
    ([TyVar]
as, Type
tbody)       = forall a. PPrint a => String -> a -> a
F.notracepp (String
"splitForallTys" forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr Type
τ) (Type -> ([TyVar], Type)
splitForAllTyCoVars Type
τ)
    su :: SortSubst
su                = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
sas (Int -> Sort
FVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  [Int
i..])
    sas :: [Symbol]
sas               = forall a. Symbolic a => a -> Symbol
symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVar]
as
    n :: Int
n                 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVar]
as
    i :: Int
i                 = Sort -> Int
sortAbs Sort
sbody forall a. Num a => a -> a -> a
+ Int
1

-- RJ: why not make this the Symbolic instance?
tyConName :: TyCon -> Symbol
tyConName :: TyCon -> Symbol
tyConName TyCon
c
  | TyCon
listTyCon forall a. Eq a => a -> a -> Bool
== TyCon
c    = Symbol
listConName
  | TyCon -> Bool
Ghc.isTupleTyCon TyCon
c = Symbol
tupConName
  | Bool
otherwise         = forall a. Symbolic a => a -> Symbol
symbol TyCon
c

typeSortFun :: TCEmb TyCon -> Type -> Sort
typeSortFun :: TCEmb TyCon -> Type -> Sort
typeSortFun TCEmb TyCon
tce Type
t = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort]
sos
  where
    sos :: [Sort]
sos           = TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
τs
    τs :: [Type]
τs            = [Type] -> Type -> [Type]
grabArgs [] Type
t

grabArgs :: [Type] -> Type -> [Type]
grabArgs :: [Type] -> Type -> [Type]
grabArgs [Type]
τs (FunTy AnonArgFlag
_ Type
_ Type
τ1 Type
τ2)
  | Just Type
a <- Type -> Maybe Type
stringClassArg Type
τ1
  = [Type] -> Type -> [Type]
grabArgs [Type]
τs ((Type -> Type) -> Type -> Type
mapType (\Type
t -> if Type
t forall a. Eq a => a -> a -> Bool
== Type
a then Type
stringTy else Type
t) Type
τ2)
  -- not ( F.notracepp ("isNonArg: " ++ GM.showPpr τ1) $ isNonValueTy τ1)
  | Bool
otherwise
  = [Type] -> Type -> [Type]
grabArgs (Type
τ1forall a. a -> [a] -> [a]
:[Type]
τs) Type
τ2
  -- otherwise
  -- = grabArgs τs τ2
  -- -- | otherwise
  -- -- = grabArgs τs τ2
grabArgs [Type]
τs Type
τ
  = forall a. [a] -> [a]
reverse (Type
τforall a. a -> [a] -> [a]
:[Type]
τs)


expandProductType :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar r))
                  => Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
expandProductType :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TyVar -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
expandProductType TyVar
x RType RTyCon RTyVar r
t
  | Bool
isTrivial'      = RType RTyCon RTyVar r
t
  | Bool
otherwise       = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar r
trep {ty_binds :: [Symbol]
ty_binds = [Symbol]
xs', ty_info :: [RFInfo]
ty_info=[RFInfo]
is', ty_args :: [RType RTyCon RTyVar r]
ty_args = [RType RTyCon RTyVar r]
ts', ty_refts :: [r]
ty_refts = [r]
rs'}
     where
      isTrivial' :: Bool
isTrivial'    = forall r. Monoid r => Type -> RRType r
ofType (TyVar -> Type
varType TyVar
x) forall a. Eq a => a -> a -> Bool
== forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t
      τs :: [Type]
τs            = forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
irrelevantMult forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> ([Scaled Type], Type)
splitFunTys forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ Type -> ([TyVar], Type)
splitForAllTyCoVars forall a b. (a -> b) -> a -> b
$ forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RType RTyCon RTyVar r
t
      trep :: RTypeRep RTyCon RTyVar r
trep          = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType RTyCon RTyVar r
t
      ([Symbol]
xs',[RFInfo]
is',[RType RTyCon RTyVar r]
ts',[r]
rs') = forall t t1 t2 t3. [(t, t1, t2, t3)] -> ([t], [t1], [t2], [t3])
unzip4 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall t r.
(Monoid t, Monoid r) =>
(Type, Symbol, RFInfo, RType RTyCon RTyVar r, t)
-> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
mkProductTy forall a b. (a -> b) -> a -> b
$ forall t t1 t2 t3 t4.
[t] -> [t1] -> [t2] -> [t3] -> [t4] -> [(t, t1, t2, t3, t4)]
zip5 [Type]
τs (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar r
trep) (forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_info RTypeRep RTyCon RTyVar r
trep) (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar r
trep) (forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar r
trep)

-- splitFunTys :: Type -> ([Type], Type)

data DataConAppContext
  = DataConAppContext
  { DataConAppContext -> DataCon
dcac_dc      :: !DataCon
  , DataConAppContext -> [Type]
dcac_tys     :: ![Type]
  , DataConAppContext -> [(Type, StrictnessMark)]
dcac_arg_tys :: ![(Type, StrictnessMark)]
  , DataConAppContext -> KindCoercion
dcac_co      :: !Coercion
  }

mkProductTy :: forall t r. (Monoid t, Monoid r)
            => (Type, Symbol, RFInfo, RType RTyCon RTyVar r, t)
            -> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
mkProductTy :: forall t r.
(Monoid t, Monoid r) =>
(Type, Symbol, RFInfo, RType RTyCon RTyVar r, t)
-> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
mkProductTy (Type
τ, Symbol
x, RFInfo
i, RType RTyCon RTyVar r
t, t
r) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(Symbol
x, RFInfo
i, RType RTyCon RTyVar r
t, t
r)] DataConAppContext -> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
f (FamInstEnvs -> Type -> Maybe DataConAppContext
deepSplitProductType FamInstEnvs
menv Type
τ)
  where
    f    :: DataConAppContext -> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
    f :: DataConAppContext -> [(Symbol, RFInfo, RType RTyCon RTyVar r, t)]
f    DataConAppContext{[(Type, StrictnessMark)]
[Type]
DataCon
KindCoercion
dcac_co :: KindCoercion
dcac_arg_tys :: [(Type, StrictnessMark)]
dcac_tys :: [Type]
dcac_dc :: DataCon
dcac_co :: DataConAppContext -> KindCoercion
dcac_arg_tys :: DataConAppContext -> [(Type, StrictnessMark)]
dcac_tys :: DataConAppContext -> [Type]
dcac_dc :: DataConAppContext -> DataCon
..} = forall a b. (a -> b) -> [a] -> [b]
map ((Symbol
dummySymbol, RFInfo
defRFInfo, , forall a. Monoid a => a
mempty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Type, StrictnessMark)]
dcac_arg_tys
    menv :: FamInstEnvs
menv = (FamInstEnv
emptyFamInstEnv, FamInstEnv
emptyFamInstEnv)

-- Copied from GHC 9.0.2.
orElse :: Maybe a -> a -> a
orElse :: forall a. Maybe a -> a -> a
orElse = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. a -> Maybe a -> a
fromMaybe

-- Copied from GHC 9.0.2.
deepSplitProductType :: FamInstEnvs -> Type -> Maybe DataConAppContext
-- If    deepSplitProductType_maybe ty = Just (dc, tys, arg_tys, co)
-- then  dc @ tys (args::arg_tys) :: rep_ty
--       co :: ty ~ rep_ty
-- Why do we return the strictness of the data-con arguments?
-- Answer: see Note [Record evaluated-ness in worker/wrapper]
deepSplitProductType :: FamInstEnvs -> Type -> Maybe DataConAppContext
deepSplitProductType FamInstEnvs
fam_envs Type
ty
  | let (KindCoercion
co, Type
ty1) = FamInstEnvs -> Type -> Maybe (KindCoercion, Type)
topNormaliseType_maybe FamInstEnvs
fam_envs Type
ty
                    forall a. Maybe a -> a -> a
`orElse` (Type -> KindCoercion
mkRepReflCo Type
ty, Type
ty)
  , Just (TyCon
tc, [Type]
tc_args) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
  , Just DataCon
con <- TyCon -> Maybe DataCon
tyConSingleDataCon_maybe TyCon
tc
  , let arg_tys :: [Scaled Type]
arg_tys = DataCon -> [Type] -> [Scaled Type]
dataConInstArgTys DataCon
con [Type]
tc_args
        strict_marks :: [StrictnessMark]
strict_marks = DataCon -> [StrictnessMark]
dataConRepStrictness DataCon
con
  = forall a. a -> Maybe a
Just DataConAppContext { dcac_dc :: DataCon
dcac_dc = DataCon
con
                           , dcac_tys :: [Type]
dcac_tys = [Type]
tc_args
                           , dcac_arg_tys :: [(Type, StrictnessMark)]
dcac_arg_tys = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
irrelevantMult [Scaled Type]
arg_tys) [StrictnessMark]
strict_marks
                           , dcac_co :: KindCoercion
dcac_co = KindCoercion
co }

deepSplitProductType FamInstEnvs
_ Type
_ = forall a. Maybe a
Nothing


-----------------------------------------------------------------------------------------
-- | Binders generated by class predicates, typically for constraining tyvars (e.g. FNum)
-----------------------------------------------------------------------------------------
classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
classBinds :: TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
classBinds TCEmb TyCon
_ (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)
  | forall c. TyConable c => c -> Bool
isFracCls RTyCon
c
  = [(forall a. Symbolic a => a -> Symbol
symbol RTyVar
a, Sort -> SortedReft
trueSortedReft Sort
FFrac) | (RVar RTyVar
a UReft Reft
_) <- [SpecType]
ts]
  | forall c. TyConable c => c -> Bool
isNumCls RTyCon
c
  = [(forall a. Symbolic a => a -> Symbol
symbol RTyVar
a, Sort -> SortedReft
trueSortedReft Sort
FNum) | (RVar RTyVar
a UReft Reft
_) <- [SpecType]
ts]
classBinds TCEmb TyCon
emb (RApp RTyCon
c [SpecType
_, SpecType
_, RVar RTyVar
a UReft Reft
_, SpecType
t] [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)
  | forall c. TyConable c => c -> Bool
isEqual RTyCon
c
  = [(forall a. Symbolic a => a -> Symbol
symbol RTyVar
a, forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb SpecType
t)]
classBinds  TCEmb TyCon
emb ty :: SpecType
ty@(RApp RTyCon
c [SpecType
_, RVar RTyVar
a UReft Reft
_, SpecType
t] [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)
  | SpecType -> Bool
isEqualityConstr SpecType
ty
  = [(forall a. Symbolic a => a -> Symbol
symbol RTyVar
a, forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb SpecType
t)]
  | Bool
otherwise
  = forall a. PPrint a => String -> a -> a
notracepp (String
"CLASSBINDS-0: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp RTyCon
c) []
classBinds TCEmb TyCon
_ SpecType
t
  = forall a. PPrint a => String -> a -> a
notracepp (String
"CLASSBINDS-1: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t, SpecType -> Bool
isEqualityConstr SpecType
t)) []

isEqualityConstr :: SpecType -> Bool
isEqualityConstr :: SpecType -> Bool
isEqualityConstr (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False -> Type
ty) = Type -> Bool
Ghc.isEqPred Type
ty Bool -> Bool -> Bool
|| Type -> Bool
Ghc.isEqPrimPred Type
ty

--------------------------------------------------------------------------------
-- | Termination Predicates ----------------------------------------------------
--------------------------------------------------------------------------------

makeNumEnv :: (Foldable t, TyConable c) => t (RType c b t1) -> [b]
makeNumEnv :: forall (t :: * -> *) c b t1.
(Foldable t, TyConable c) =>
t (RType c b t1) -> [b]
makeNumEnv = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {c} {a} {r}. TyConable c => RType c a r -> [a]
go
  where
    go :: RType c a r -> [a]
go (RApp c
c [RType c a r]
ts [RTProp c a r]
_ r
_) | forall c. TyConable c => c -> Bool
isNumCls c
c Bool -> Bool -> Bool
|| forall c. TyConable c => c -> Bool
isFracCls c
c = [ a
a | (RVar a
a r
_) <- [RType c a r]
ts]
    go RType c a r
_ = []

isDecreasing :: S.HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing :: HashSet TyCon -> [RTyVar] -> SpecType -> Bool
isDecreasing HashSet TyCon
autoenv  [RTyVar]
_ (RApp RTyCon
c [SpecType]
_ [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)
  =  forall a. Maybe a -> Bool
isJust (TyConInfo -> Maybe SizeFun
sizeFunction (RTyCon -> TyConInfo
rtc_info RTyCon
c)) -- user specified size or
  Bool -> Bool -> Bool
|| HashSet TyCon -> TyCon -> Bool
isSizeable HashSet TyCon
autoenv TyCon
tc
  where tc :: TyCon
tc = RTyCon -> TyCon
rtc_tc RTyCon
c
isDecreasing HashSet TyCon
_ [RTyVar]
cenv (RVar RTyVar
v UReft Reft
_)
  = RTyVar
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RTyVar]
cenv
isDecreasing HashSet TyCon
_ [RTyVar]
_ SpecType
_
  = Bool
False

makeDecrType :: Symbolic a
             => S.HashSet TyCon
             -> Maybe (a, (Symbol, RType RTyCon t (UReft Reft)))
             -> Either (Symbol, RType RTyCon t (UReft Reft)) String
makeDecrType :: forall a t.
Symbolic a =>
HashSet TyCon
-> Maybe (a, (Symbol, RType RTyCon t (UReft Reft)))
-> Either (Symbol, RType RTyCon t (UReft Reft)) String
makeDecrType HashSet TyCon
autoenv (Just (a
v, (Symbol
x, RType RTyCon t (UReft Reft)
t)))
  = forall a b. a -> Either a b
Left (Symbol
x, RType RTyCon t (UReft Reft)
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` UReft Reft
tr)
  where
    tr :: UReft Reft
tr  = forall r. r -> UReft r
uTop forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
Reft (forall {a}. IsString a => a
vv', [Expr] -> Expr
pOr [Expr
r])
    r :: Expr
r   = forall t. (t, t, t -> Expr) -> Expr
cmpLexRef (Symbol
v', forall {a}. IsString a => a
vv', Symbol -> Expr
f)
    v' :: Symbol
v'  = forall a. Symbolic a => a -> Symbol
symbol a
v
    f :: Symbol -> Expr
f   = forall t t1. HashSet TyCon -> RType RTyCon t t1 -> Symbol -> Expr
mkDecrFun HashSet TyCon
autoenv RType RTyCon t (UReft Reft)
t
    vv' :: a
vv' = a
"vvRec"

makeDecrType HashSet TyCon
_ Maybe (a, (Symbol, RType RTyCon t (UReft Reft)))
_
  = forall a b. b -> Either a b
Right String
"RefType.makeDecrType called on invalid input"

isSizeable  :: S.HashSet TyCon -> TyCon -> Bool
isSizeable :: HashSet TyCon -> TyCon -> Bool
isSizeable HashSet TyCon
autoenv TyCon
tc = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyCon
tc HashSet TyCon
autoenv --   Ghc.isAlgTyCon tc -- && Ghc.isRecursiveTyCon tc

mkDecrFun :: S.HashSet TyCon -> RType RTyCon t t1 -> Symbol -> Expr
mkDecrFun :: forall t t1. HashSet TyCon -> RType RTyCon t t1 -> Symbol -> Expr
mkDecrFun HashSet TyCon
autoenv (RApp RTyCon
c [RType RTyCon t t1]
_ [RTProp RTyCon t t1]
_ t1
_)
  | Just Symbol -> Expr
f <- SizeFun -> Symbol -> Expr
szFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> Maybe SizeFun
sizeFunction (RTyCon -> TyConInfo
rtc_info RTyCon
c)
  = Symbol -> Expr
f
  | HashSet TyCon -> TyCon -> Bool
isSizeable HashSet TyCon
autoenv forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
c
  = \Symbol
v -> LocSymbol -> [Expr] -> Expr
F.mkEApp LocSymbol
lenLocSymbol [Symbol -> Expr
F.EVar Symbol
v]
mkDecrFun HashSet TyCon
_ (RVar t
_ t1
_)
  = Symbol -> Expr
EVar
mkDecrFun HashSet TyCon
_ RType RTyCon t t1
_
  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType.mkDecrFun called on invalid input"

-- | [NOTE]: THIS IS WHERE THE TERMINATION METRIC REFINEMENTS ARE CREATED.
cmpLexRef :: (t, t, t -> Expr) -> Expr
cmpLexRef :: forall t. (t, t, t -> Expr) -> Expr
cmpLexRef (t
v, t
x, t -> Expr
g)
  = [Expr] -> Expr
pAnd [Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt (t -> Expr
g t
x) (t -> Expr
g t
v), Brel -> Expr -> Expr -> Expr
PAtom Brel
Ge (t -> Expr
g t
x) Expr
zero]
  where zero :: Expr
zero = Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0

makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft
makeLexRefa :: [Located Expr] -> [Located Expr] -> UReft Reft
makeLexRefa [Located Expr]
es' [Located Expr]
es = forall r. r -> UReft r
uTop forall a b. (a -> b) -> a -> b
$ (Symbol, Expr) -> Reft
Reft (forall {a}. IsString a => a
vv', Expr -> Expr -> Expr
PIff (Symbol -> Expr
EVar forall {a}. IsString a => a
vv') forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pOr [Expr]
rs)
  where
    rs :: [Expr]
rs  = [(Expr, Expr)] -> [Expr] -> [Expr] -> [Expr] -> [Expr]
makeLexReft [] [] (forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located Expr]
es) (forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located Expr]
es')
    vv' :: a
vv' = a
"vvRec"

makeLexReft :: [(Expr, Expr)] -> [Expr] -> [Expr] -> [Expr] -> [Expr]
makeLexReft :: [(Expr, Expr)] -> [Expr] -> [Expr] -> [Expr] -> [Expr]
makeLexReft [(Expr, Expr)]
_ [Expr]
acc [] []
  = [Expr]
acc
makeLexReft [(Expr, Expr)]
old [Expr]
acc (Expr
e:[Expr]
es) (Expr
e':[Expr]
es')
  = [(Expr, Expr)] -> [Expr] -> [Expr] -> [Expr] -> [Expr]
makeLexReft ((Expr
e,Expr
e')forall a. a -> [a] -> [a]
:[(Expr, Expr)]
old) (Expr
rforall a. a -> [a] -> [a]
:[Expr]
acc) [Expr]
es [Expr]
es'
  where
    r :: Expr
r    = [Expr] -> Expr
pAnd forall a b. (a -> b) -> a -> b
$   Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt Expr
e' Expr
e
                forall a. a -> [a] -> [a]
:   Brel -> Expr -> Expr -> Expr
PAtom Brel
Ge Expr
e' Expr
zero
                forall a. a -> [a] -> [a]
:  [Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq Expr
o' Expr
o    | (Expr
o,Expr
o') <- [(Expr, Expr)]
old]
                forall a. [a] -> [a] -> [a]
++ [Brel -> Expr -> Expr -> Expr
PAtom Brel
Ge Expr
o' Expr
zero | (Expr
_,Expr
o') <- [(Expr, Expr)]
old]
    zero :: Expr
zero = Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0
makeLexReft [(Expr, Expr)]
_ [Expr]
_ [Expr]
_ [Expr]
_
  = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"RefType.makeLexReft on invalid input"

--------------------------------------------------------------------------------
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
mkTyConInfo :: TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
mkTyConInfo TyCon
c VarianceInfo
userTv VarianceInfo
userPv Maybe SizeFun
f = VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
TyConInfo VarianceInfo
tcTv VarianceInfo
userPv Maybe SizeFun
f
  where
    tcTv :: VarianceInfo
tcTv                      = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null VarianceInfo
userTv then VarianceInfo
defTv else VarianceInfo
userTv
    defTv :: VarianceInfo
defTv                     = TyCon -> VarianceInfo
makeTyConVariance TyCon
c


--------------------------------------------------------------------------------
-- | Printing Refinement Types -------------------------------------------------
--------------------------------------------------------------------------------

instance Show RTyVar where
  show :: RTyVar -> String
show = forall a. PPrint a => a -> String
showpp

instance PPrint (UReft r) => Show (UReft r) where
  show :: UReft r -> String
show = forall a. PPrint a => a -> String
showpp

instance PPrint DataDecl where
  pprintTidy :: Tidy -> DataDecl -> Doc
pprintTidy Tidy
k DataDecl
dd =
    let
      prefix :: Doc
prefix = Doc
"data" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint (DataDecl -> DataName
tycName DataDecl
dd) Doc -> Doc -> Doc
<+> Maybe SizeFun -> Doc
ppMbSizeFun (DataDecl -> Maybe SizeFun
tycSFun DataDecl
dd) Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint (DataDecl -> [Symbol]
tycTyVars DataDecl
dd)
    in
      case DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
dd of
        Maybe [DataCtor]
Nothing   -> Doc
prefix
        Just [DataCtor]
cons -> Doc
prefix Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ([Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ [ Doc
"|" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k DataCtor
c | DataCtor
c <- [DataCtor]
cons ])

instance PPrint DataCtor where
  -- pprintTidy k (DataCtor c as _   xts Nothing)  = pprintTidy k c <+> dcolon ppVars as <+> braces (ppFields k ", " xts)
  -- pprintTidy k (DataCtor c as ths xts (Just t)) = pprintTidy k c <+> dcolon <+> ppVars as <+> ppThetas ths <+> (ppFields k " ->" xts) <+> "->" <+> pprintTidy k t
  pprintTidy :: Tidy -> DataCtor -> Doc
pprintTidy Tidy
k (DataCtor LocSymbol
c [Symbol]
as [RType BTyCon BTyVar (UReft Reft)]
ths [(Symbol, RType BTyCon BTyVar (UReft Reft))]
xts Maybe (RType BTyCon BTyVar (UReft Reft))
t) = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k LocSymbol
c Doc -> Doc -> Doc
<+> Doc
dcolon Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> [a] -> Doc
ppVars Tidy
k [Symbol]
as Doc -> Doc -> Doc
<+> [RType BTyCon BTyVar (UReft Reft)] -> Doc
ppThetas [RType BTyCon BTyVar (UReft Reft)]
ths Doc -> Doc -> Doc
<+> forall k v. (PPrint k, PPrint v) => Tidy -> Doc -> [(k, v)] -> Doc
ppFields Tidy
k Doc
" ->" [(Symbol, RType BTyCon BTyVar (UReft Reft))]
xts Doc -> Doc -> Doc
<+> Doc
"->" Doc -> Doc -> Doc
<+> Doc
res
    where
      res :: Doc
res         = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"*" (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k) Maybe (RType BTyCon BTyVar (UReft Reft))
t
      ppThetas :: [RType BTyCon BTyVar (UReft Reft)] -> Doc
ppThetas [] = Doc
empty
      ppThetas [RType BTyCon BTyVar (UReft Reft)]
ts = Doc -> Doc
parens ([Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
", " (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType BTyCon BTyVar (UReft Reft)]
ts)) Doc -> Doc -> Doc
<+> Doc
"=>"


ppVars :: (PPrint a) => Tidy -> [a] -> Doc
ppVars :: forall a. PPrint a => Tidy -> [a] -> Doc
ppVars Tidy
k [a]
as = Doc
"forall" Doc -> Doc -> Doc
<+> [Doc] -> Doc
hcat (Doc -> [Doc] -> [Doc]
punctuate Doc
" " (forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
as)) Doc -> Doc -> Doc
<+> Doc
"."

ppFields :: (PPrint k, PPrint v) => Tidy -> Doc -> [(k, v)] -> Doc
ppFields :: forall k v. (PPrint k, PPrint v) => Tidy -> Doc -> [(k, v)] -> Doc
ppFields Tidy
k Doc
sep' [(k, v)]
kvs = [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
sep' (forall a. PPrint a => Tidy -> a -> Doc
F.pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(k, v)]
kvs)

ppMbSizeFun :: Maybe SizeFun -> Doc
ppMbSizeFun :: Maybe SizeFun -> Doc
ppMbSizeFun Maybe SizeFun
Nothing  = Doc
""
ppMbSizeFun (Just SizeFun
z) = forall a. PPrint a => a -> Doc
F.pprint SizeFun
z

-- instance PPrint DataCtor where
  -- pprintTidy k (DataCtor c xts t) =
    -- pprintTidy k c <+> text "::" <+> (hsep $ punctuate (text "->")
                                          -- ((pprintTidy k <$> xts) ++ [pprintTidy k t]))

-- ppHack :: (?callStack :: CallStack) => a -> b
-- ppHack _ = errorstar "OOPS"

instance PPrint (RType c tv r) => Show (RType c tv r) where
  show :: RType c tv r -> String
show = forall a. PPrint a => a -> String
showpp

instance PPrint (RTProp c tv r) => Show (RTProp c tv r) where
  show :: RTProp c tv r -> String
show = forall a. PPrint a => a -> String
showpp


-------------------------------------------------------------------------------
-- | tyVarsPosition t returns the type variables appearing
-- | (in positive positions, in negative positions, in undetermined positions)
-- | undetermined positions are due to type constructors and type application
-------------------------------------------------------------------------------
tyVarsPosition :: RType RTyCon tv r -> Positions tv
tyVarsPosition :: forall tv r. RType RTyCon tv r -> Positions tv
tyVarsPosition = forall {a} {r}. Maybe Bool -> RType RTyCon a r -> Positions a
go (forall a. a -> Maybe a
Just Bool
True)
  where
    go :: Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p (RVar a
t r
_)         = forall {a}. Maybe Bool -> a -> Positions a
report Maybe Bool
p a
t
    go Maybe Bool
p (RFun Symbol
_ RFInfo
_ RType RTyCon a r
t1 RType RTyCon a r
t2 r
_) = Maybe Bool -> RType RTyCon a r -> Positions a
go (forall {f :: * -> *}. Functor f => f Bool -> f Bool
flip' Maybe Bool
p) RType RTyCon a r
t1 forall a. Semigroup a => a -> a -> a
<> Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t2
    go Maybe Bool
p (RAllT RTVU RTyCon a
_ RType RTyCon a r
t r
_)      = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t
    go Maybe Bool
p (RAllP PVU RTyCon a
_ RType RTyCon a r
t)        = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t
    go Maybe Bool
p (RApp RTyCon
c [RType RTyCon a r]
ts [RTProp RTyCon a r]
_ r
_)    = forall a. Monoid a => [a] -> a
mconcat (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Maybe Bool -> RType RTyCon a r -> Positions a
go (Maybe Bool -> Variance -> Maybe Bool
getPosition Maybe Bool
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> VarianceInfo
varianceTyArgs (RTyCon -> TyConInfo
rtc_info RTyCon
c)) [RType RTyCon a r]
ts)
    go Maybe Bool
p (RAllE Symbol
_ RType RTyCon a r
t1 RType RTyCon a r
t2)    = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t1 forall a. Semigroup a => a -> a -> a
<> Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t2
    go Maybe Bool
p (REx Symbol
_ RType RTyCon a r
t1 RType RTyCon a r
t2)      = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t1 forall a. Semigroup a => a -> a -> a
<> Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t2
    go Maybe Bool
_ (RExprArg Located Expr
_)       = forall a. Monoid a => a
mempty
    go Maybe Bool
p (RAppTy RType RTyCon a r
t1 RType RTyCon a r
t2 r
_)   = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t1 forall a. Semigroup a => a -> a -> a
<> Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t2
    go Maybe Bool
p (RRTy [(Symbol, RType RTyCon a r)]
_ r
_ Oblig
_ RType RTyCon a r
t)     = Maybe Bool -> RType RTyCon a r -> Positions a
go Maybe Bool
p RType RTyCon a r
t
    go Maybe Bool
_ (RHole r
_)          = forall a. Monoid a => a
mempty

    getPosition :: Maybe Bool -> Variance -> Maybe Bool
    getPosition :: Maybe Bool -> Variance -> Maybe Bool
getPosition Maybe Bool
b Variance
Contravariant = Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Bool
b
    getPosition Maybe Bool
b Variance
_             = Maybe Bool
b

    report :: Maybe Bool -> a -> Positions a
report (Just Bool
True)  a
v = forall a. [a] -> [a] -> [a] -> Positions a
Pos [a
v] []  []
    report (Just Bool
False) a
v = forall a. [a] -> [a] -> [a] -> Positions a
Pos []  [a
v] []
    report Maybe Bool
Nothing a
v      = forall a. [a] -> [a] -> [a] -> Positions a
Pos []  []  [a
v]
    flip' :: f Bool -> f Bool
flip' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not

data Positions a = Pos {forall a. Positions a -> [a]
ppos :: [a], forall a. Positions a -> [a]
pneg :: [a], forall a. Positions a -> [a]
punknown :: [a]}

instance Monoid (Positions a) where
  mempty :: Positions a
mempty = forall a. [a] -> [a] -> [a] -> Positions a
Pos [] [] []
instance Semigroup (Positions a) where
  (Pos [a]
x1 [a]
x2 [a]
x3) <> :: Positions a -> Positions a -> Positions a
<> (Pos [a]
y1 [a]
y2 [a]
y3) = forall a. [a] -> [a] -> [a] -> Positions a
Pos ([a]
x1 forall a. [a] -> [a] -> [a]
++ [a]
y1) ([a]
x2 forall a. [a] -> [a] -> [a]
++ [a]
y2) ([a]
x3 forall a. [a] -> [a] -> [a]
++ [a]
y3)