{-# LANGUAGE FlexibleContexts #-}
module Language.Haskell.Liquid.LawInstances ( checkLawInstances ) where

import qualified Data.List                                  as L
import qualified Data.Maybe                                 as Mb
import           Text.PrettyPrint.HughesPJ                  hiding ((<>))

import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Types.Equality
import           Language.Haskell.Liquid.GHC.API
import qualified Language.Fixpoint.Types                     as F

checkLawInstances :: GhcSpecLaws -> Diagnostics
checkLawInstances :: GhcSpecLaws -> Diagnostics
checkLawInstances GhcSpecLaws
speclaws = (LawInstance -> Diagnostics) -> [LawInstance] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap LawInstance -> Diagnostics
go (GhcSpecLaws -> [LawInstance]
gsLawInst GhcSpecLaws
speclaws)
  where go :: LawInstance -> Diagnostics
go LawInstance
l = Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance (LawInstance -> Class
lilName LawInstance
l) ([(Var, LocSpecType)]
-> Maybe [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (Maybe [(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> Maybe [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ Class
-> [(Class, [(Var, LocSpecType)])] -> Maybe [(Var, LocSpecType)]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (LawInstance -> Class
lilName LawInstance
l) (GhcSpecLaws -> [(Class, [(Var, LocSpecType)])]
gsLawDefs GhcSpecLaws
speclaws)) LawInstance
l

checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance :: Class -> [(Var, LocSpecType)] -> LawInstance -> Diagnostics
checkOneInstance Class
c [(Var, LocSpecType)]
laws LawInstance
li
  = Class
-> LawInstance
-> [Var]
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> Diagnostics
checkExtra Class
c LawInstance
li (((Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, LocSpecType) -> Var) -> [(Var, LocSpecType)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, LocSpecType)]
laws) [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Class -> [Var]
classMethods Class
c) (LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li) Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Var, LocSpecType)
l -> Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw Class
c (Var, LocSpecType)
l LawInstance
li) [(Var, LocSpecType)]
laws

checkExtra :: Class
           -> LawInstance
           -> [Var]
           -> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
           -> Diagnostics
checkExtra :: Class
-> LawInstance
-> [Var]
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> Diagnostics
checkExtra Class
c LawInstance
li [Var]
_laws [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts =
    let allMsgs :: [Doc]
allMsgs = {- (msgExtra <$> extra) ++ -} (LocSymbol -> Doc
forall a. PPrint a => a -> Doc
msgUnfoundLaw (LocSymbol -> Doc) -> [LocSymbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
unfoundLaws) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (LocSymbol -> Doc
forall a. PPrint a => a -> Doc
msgUnfoundInstance (LocSymbol -> Doc) -> [LocSymbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSymbol]
unfoundInstances)
    in [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (Doc -> Error
forall t. Doc -> TError t
mkError (Doc -> Error) -> [Doc] -> [Error]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
allMsgs)
    where
        unfoundInstances :: [LocSymbol]
unfoundInstances = [ LocSymbol
x | (VarOrLocSymbol
_, (Right LocSymbol
x,Maybe LocSpecType
_)) <- [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts]
        unfoundLaws :: [LocSymbol]
unfoundLaws = [ LocSymbol
x | (Right LocSymbol
x, (VarOrLocSymbol, Maybe LocSpecType)
_) <- [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
insts]
        _extra :: [a]
_extra = [] -- this breaks on extra super requirements [ (x,i) | (Left x, (Left i, _)) <- insts, not (x `L.elem` laws)] 
        mkError :: Doc -> TError t
mkError = SrcSpan -> Doc -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrILaw (LawInstance -> SrcSpan
lilPos LawInstance
li) (Class -> Doc
forall a. PPrint a => a -> Doc
pprint Class
c) ([LocSpecType] -> Doc
forall a. PPrint a => a -> Doc
pprint ([LocSpecType] -> Doc) -> [LocSpecType] -> Doc
forall a b. (a -> b) -> a -> b
$ LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)
        _msgExtra :: (a, b) -> Doc
_msgExtra (a
x,b
_)      = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined law."
        msgUnfoundLaw :: a -> Doc
msgUnfoundLaw a
i      = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
i Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined law."
        msgUnfoundInstance :: a -> Doc
msgUnfoundInstance a
i = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
i Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not a defined instance."

checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw :: Class -> (Var, LocSpecType) -> LawInstance -> Diagnostics
checkOneLaw Class
c (Var
x, LocSpecType
t) LawInstance
li
  | Just (Left Var
_, Just LocSpecType
ti) <- Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix
  = (Doc -> Error)
-> Class
-> LawInstance
-> LocSpecType
-> LocSpecType
-> Diagnostics
unify Doc -> Error
forall t. Doc -> TError t
mkError Class
c LawInstance
li LocSpecType
t LocSpecType
ti
  | Just (Right LocSymbol
_l, Maybe LocSpecType
_) <- Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix
  = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Doc -> Error
forall t. Doc -> TError t
mkError (String -> Doc
text String
"is not found.")]
  | Bool
otherwise
  = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Doc -> Error
forall t. Doc -> TError t
mkError (String -> Doc
text String
"is not defined.")]
  where
    lix :: Maybe (VarOrLocSymbol, Maybe LocSpecType)
lix = VarOrLocSymbol
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
-> Maybe (VarOrLocSymbol, Maybe LocSpecType)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (Var -> VarOrLocSymbol
forall a b. a -> Either a b
Left Var
x) (LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li)
    mkError :: Doc -> TError t
mkError Doc
txt = SrcSpan -> Doc -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> Doc -> TError t
ErrILaw (LawInstance -> SrcSpan
lilPos LawInstance
li) (Class -> Doc
forall a. PPrint a => a -> Doc
pprint Class
c) ([LocSpecType] -> Doc
forall a. PPrint a => [a] -> Doc
pprintXs ([LocSpecType] -> Doc) -> [LocSpecType] -> Doc
forall a b. (a -> b) -> a -> b
$ LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)
                          (String -> Doc
text String
"The instance for the law" Doc -> Doc -> Doc
<+> Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
x Doc -> Doc -> Doc
<+> Doc
txt)
    pprintXs :: [a] -> Doc
pprintXs [a
l] = a -> Doc
forall a. PPrint a => a -> Doc
pprint a
l
    pprintXs [a]
xs  = [a] -> Doc
forall a. PPrint a => a -> Doc
pprint [a]
xs

unify :: (Doc -> Error) -> Class -> LawInstance -> LocSpecType -> LocSpecType -> Diagnostics
unify :: (Doc -> Error)
-> Class
-> LawInstance
-> LocSpecType
-> LocSpecType
-> Diagnostics
unify Doc -> Error
mkError Class
c LawInstance
li LocSpecType
t1 LocSpecType
t2
  = if RType RTyCon RTyVar RReft
t11 RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft -> Bool
forall a. REq a => a -> a -> Bool
=*= RType RTyCon RTyVar RReft
t22 then Diagnostics
emptyDiagnostics else Diagnostics
err
  where
    err :: Diagnostics
err = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Doc -> Error
mkError (String -> Doc
text String
"is invalid:\nType" Doc -> Doc -> Doc
<+> LocSpecType -> Doc
forall a. PPrint a => a -> Doc
pprint LocSpecType
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"\nis different than\n" Doc -> Doc -> Doc
<+> LocSpecType -> Doc
forall a. PPrint a => a -> Doc
pprint LocSpecType
t2
       --  text "\nesubt1 = " <+> pprint esubst1  
       -- text "\nesubt = " <+> pprint esubst  
       -- text "\ncompared\n" <+> pprint t11 <+> text "\nWITH\n" <+> pprint t22 
           )]

    t22 :: RType RTyCon RTyVar RReft
t22 = RTypeRep RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft
trep2 {ty_vars :: [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
ty_vars = [], ty_binds :: [Symbol]
ty_binds = (Symbol, RType RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RType RTyCon RTyVar RReft) -> Symbol)
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args2, ty_args :: [RType RTyCon RTyVar RReft]
ty_args = (Symbol, RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall a b. (a, b) -> b
snd ((Symbol, RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft)
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> [RType RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args2, ty_refts :: [RReft]
ty_refts = Int -> [RReft] -> [RReft]
forall a. Int -> [a] -> [a]
drop ([(Symbol, RType RTyCon RTyVar RReft)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar RReft)]
tc2) (RTypeRep RTyCon RTyVar RReft -> [RReft]
forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar RReft
trep2)})
    t11 :: RType RTyCon RTyVar RReft
t11 = RTypeRep RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (RTypeRep RTyCon RTyVar RReft
trep1 { ty_vars :: [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
ty_vars = []
                              , ty_binds :: [Symbol]
ty_binds = (Symbol, RType RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RType RTyCon RTyVar RReft) -> Symbol)
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args2
                              , ty_args :: [RType RTyCon RTyVar RReft]
ty_args = (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tx (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> ((Symbol, RType RTyCon RTyVar RReft)
    -> RType RTyCon RTyVar RReft)
-> (Symbol, RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft
forall a b. (a, b) -> b
snd) ((Symbol, RType RTyCon RTyVar RReft) -> RType RTyCon RTyVar RReft)
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> [RType RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args1
                              , ty_refts :: [RReft]
ty_refts = Subst -> RReft -> RReft
forall a. Subable a => Subst -> a -> a
F.subst Subst
esubst (RReft -> RReft) -> [RReft] -> [RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [RReft] -> [RReft]
forall a. Int -> [a] -> [a]
drop ([(Symbol, RType RTyCon RTyVar RReft)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar RReft)]
tc1) (RTypeRep RTyCon RTyVar RReft -> [RReft]
forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar RReft
trep1)
                              , ty_res :: RType RTyCon RTyVar RReft
ty_res = RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tx (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep1})
    tx :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tx = [(Var, Type)]
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
subtsSpec [(Var, Type)]
tsubst (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. Subable a => Subst -> a -> a
F.subst Subst
esubst
    subtsSpec :: [(Var, Type)]
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
subtsSpec = [(Var, Type)]
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts :: ([(TyVar, Type)] -> SpecType -> SpecType)

    trep1 :: RTypeRep RTyCon RTyVar RReft
trep1 = RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val LocSpecType
t1 
    trep2 :: RTypeRep RTyCon RTyVar RReft
trep2 = RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RTypeRep RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val LocSpecType
t2 
    ([(Symbol, RType RTyCon RTyVar RReft)]
tc1, [(Symbol, RType RTyCon RTyVar RReft)]
args1) = [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
splitTypeConstraints ([(Symbol, RType RTyCon RTyVar RReft)]
 -> ([(Symbol, RType RTyCon RTyVar RReft)],
     [(Symbol, RType RTyCon RTyVar RReft)]))
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [RType RTyCon RTyVar RReft]
-> [(Symbol, RType RTyCon RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep1) (RTypeRep RTyCon RTyVar RReft -> [RType RTyCon RTyVar RReft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep1)
    ([(Symbol, RType RTyCon RTyVar RReft)]
tc2, [(Symbol, RType RTyCon RTyVar RReft)]
args2) = [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
splitTypeConstraints ([(Symbol, RType RTyCon RTyVar RReft)]
 -> ([(Symbol, RType RTyCon RTyVar RReft)],
     [(Symbol, RType RTyCon RTyVar RReft)]))
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [RType RTyCon RTyVar RReft]
-> [(Symbol, RType RTyCon RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep2) (RTypeRep RTyCon RTyVar RReft -> [RType RTyCon RTyVar RReft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep2)
    esubst :: Subst
esubst = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)]
esubst1
                 [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. [a] -> [a] -> [a]
++  [(Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x, Symbol -> Expr
F.EVar (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
y)) | (Left Var
x, (Left Var
y, Maybe LocSpecType
_)) <- LawInstance
-> [(VarOrLocSymbol, (VarOrLocSymbol, Maybe LocSpecType))]
lilEqus LawInstance
li]
                     )
    esubst1 :: [(Symbol, Expr)]
esubst1 = [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip  ((Symbol, RType RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RType RTyCon RTyVar RReft) -> Symbol)
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args1) ((Symbol -> Expr
F.EVar (Symbol -> Expr)
-> ((Symbol, RType RTyCon RTyVar RReft) -> Symbol)
-> (Symbol, RType RTyCon RTyVar RReft)
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RType RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst) ((Symbol, RType RTyCon RTyVar RReft) -> Expr)
-> [(Symbol, RType RTyCon RTyVar RReft)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType RTyCon RTyVar RReft)]
args2)

    tsubst :: [(Var, Type)]
tsubst = [(Var, Type)] -> [(Var, Type)]
forall a. [a] -> [a]
reverse ([(Var, Type)] -> [(Var, Type)]) -> [(Var, Type)] -> [(Var, Type)]
forall a b. (a -> b) -> a -> b
$ [Var] -> [Type] -> [(Var, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((\(RTV Var
v) -> Var
v) (RTyVar -> Var) -> [RTyVar] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(Symbol, RType RTyCon RTyVar RReft)] -> [RTyVar]
forall a a r. [(a, RType RTyCon a r)] -> [a]
findTyVars [(Symbol, RType RTyCon RTyVar RReft)]
tc1 [RTyVar] -> [RTyVar] -> [RTyVar]
forall a. [a] -> [a] -> [a]
++ (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar)
-> [RTVar RTyVar (RType RTyCon RTyVar ())] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[RTVar RTyVar (RType RTyCon RTyVar ())]]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[RTVar RTyVar (RType RTyCon RTyVar ())]]
argVars)))
                 (RType RTyCon RTyVar RReft -> Type
forall r. ToTypeable r => RRType r -> Type
toType (RType RTyCon RTyVar RReft -> Type)
-> [RType RTyCon RTyVar RReft] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([RType RTyCon RTyVar RReft]
argBds [RType RTyCon RTyVar RReft]
-> [RType RTyCon RTyVar RReft] -> [RType RTyCon RTyVar RReft]
forall a. [a] -> [a] -> [a]
++ (((RTyVar -> RReft -> RType RTyCon RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
`RVar` RReft
forall a. Monoid a => a
mempty) (RTyVar -> RType RTyCon RTyVar RReft)
-> (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar)
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value) (RTVar RTyVar (RType RTyCon RTyVar ())
 -> RType RTyCon RTyVar RReft)
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RType RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((RTVar RTyVar (RType RTyCon RTyVar ()), RReft)
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall a b. (a, b) -> a
fst ((RTVar RTyVar (RType RTyCon RTyVar ()), RReft)
 -> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeRep RTyCon RTyVar RReft
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall c tv r. RTypeRep c tv r -> [(RTVar tv (RType c tv ()), r)]
ty_vars RTypeRep RTyCon RTyVar RReft
trep2))))

    ([[RTVar RTyVar (RType RTyCon RTyVar ())]]
argVars, [RType RTyCon RTyVar RReft]
argBds) = [([RTVar RTyVar (RType RTyCon RTyVar ())],
  RType RTyCon RTyVar RReft)]
-> ([[RTVar RTyVar (RType RTyCon RTyVar ())]],
    [RType RTyCon RTyVar RReft])
forall a b. [(a, b)] -> ([a], [b])
unzip ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar RReft
-> ([RTVar RTyVar (RType RTyCon RTyVar ())],
    RType RTyCon RTyVar RReft)
forall c tv r.
[RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall [] (RType RTyCon RTyVar RReft
 -> ([RTVar RTyVar (RType RTyCon RTyVar ())],
     RType RTyCon RTyVar RReft))
-> (LocSpecType -> RType RTyCon RTyVar RReft)
-> LocSpecType
-> ([RTVar RTyVar (RType RTyCon RTyVar ())],
    RType RTyCon RTyVar RReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> RType RTyCon RTyVar RReft
forall a. Located a -> a
val (LocSpecType
 -> ([RTVar RTyVar (RType RTyCon RTyVar ())],
     RType RTyCon RTyVar RReft))
-> [LocSpecType]
-> [([RTVar RTyVar (RType RTyCon RTyVar ())],
     RType RTyCon RTyVar RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LawInstance -> [LocSpecType]
lilTyArgs LawInstance
li)

    splitForall :: [RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall [RTVU c tv]
vs (RAllT RTVU c tv
v RType c tv r
t r
_) = [RTVU c tv] -> RType c tv r -> ([RTVU c tv], RType c tv r)
splitForall (RTVU c tv
vRTVU c tv -> [RTVU c tv] -> [RTVU c tv]
forall a. a -> [a] -> [a]
:[RTVU c tv]
vs) RType c tv r
t 
    splitForall [RTVU c tv]
vs  RType c tv r
t            = ([RTVU c tv]
vs, RType c tv r
t) 

    findTyVars :: [(a, RType RTyCon a r)] -> [a]
findTyVars (((a
_x, RApp RTyCon
cc [RType RTyCon a r]
as [RTProp RTyCon a r]
_ r
_):[(a, RType RTyCon a r)]
_ts)) | RTyCon -> TyCon
rtc_tc RTyCon
cc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== Class -> TyCon
classTyCon Class
c 
      = [a
v | RVar a
v r
_ <- [RType RTyCon a r]
as ]
    findTyVars ((a, RType RTyCon a r)
_:[(a, RType RTyCon a r)]
ts) = [(a, RType RTyCon a r)] -> [a]
findTyVars [(a, RType RTyCon a r)]
ts 
    findTyVars [] = [] 


splitTypeConstraints :: [(F.Symbol, SpecType)] -> ([(F.Symbol, SpecType)], [(F.Symbol, SpecType)])
splitTypeConstraints :: [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
splitTypeConstraints = [(Symbol, RType RTyCon RTyVar RReft)]
-> [(Symbol, RType RTyCon RTyVar RReft)]
-> ([(Symbol, RType RTyCon RTyVar RReft)],
    [(Symbol, RType RTyCon RTyVar RReft)])
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
[(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go []  
  where  
    go :: [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go [(Symbol, RType c tv (f Reft))]
cs (b :: (Symbol, RType c tv (f Reft))
b@(Symbol
_x, RApp c
c [RType c tv (f Reft)]
_ [RTProp c tv (f Reft)]
_ f Reft
_):[(Symbol, RType c tv (f Reft))]
ts) 
      | c -> Bool
forall c. TyConable c => c -> Bool
isClass c
c
      = [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
-> ([(Symbol, RType c tv (f Reft))],
    [(Symbol, RType c tv (f Reft))])
go ((Symbol, RType c tv (f Reft))
b(Symbol, RType c tv (f Reft))
-> [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
forall a. a -> [a] -> [a]
:[(Symbol, RType c tv (f Reft))]
cs) [(Symbol, RType c tv (f Reft))]
ts 
    go [(Symbol, RType c tv (f Reft))]
cs [(Symbol, RType c tv (f Reft))]
r = ([(Symbol, RType c tv (f Reft))] -> [(Symbol, RType c tv (f Reft))]
forall a. [a] -> [a]
reverse [(Symbol, RType c tv (f Reft))]
cs, ((Symbol, RType c tv (f Reft)) -> (Symbol, RType c tv (f Reft)))
-> [(Symbol, RType c tv (f Reft))]
-> [(Symbol, RType c tv (f Reft))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
x, RType c tv (f Reft)
t) -> (Symbol
x, RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV RType c tv (f Reft)
t Symbol
x)) [(Symbol, RType c tv (f Reft))]
r)