{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Language.Haskell.Liquid.Bare.Class
( makeClasses
, makeSpecDictionaries
, makeDefaultMethods
, makeMethodTypes
)
where
import Data.Bifunctor
import qualified Data.Maybe as Mb
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Types.Visitor as F
import Language.Haskell.Liquid.Types.Dictionaries
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Liquid.GHC.API as Ghc
import Language.Haskell.Liquid.Misc
import Language.Haskell.Liquid.Types.DataDecl
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.Visitors
import qualified Language.Haskell.Liquid.Measure as Ms
import Language.Haskell.Liquid.Bare.Types as Bare
import Language.Haskell.Liquid.Bare.Resolve as Bare
import Language.Haskell.Liquid.Bare.Expand as Bare
import Language.Haskell.Liquid.Bare.Misc as Bare
import Text.PrettyPrint.HughesPJ (text)
import qualified Control.Exception as Ex
import Control.Monad (forM)
makeMethodTypes :: Bool -> DEnv Ghc.Var LocSpecType -> [DataConP] -> [Ghc.CoreBind] -> [(Ghc.Var, MethodType LocSpecType)]
makeMethodTypes :: Bool
-> DEnv Var LocSpecType
-> [DataConP]
-> [CoreBind]
-> [(Var, MethodType LocSpecType)]
makeMethodTypes Bool
allowTC (DEnv HashMap Var (HashMap Symbol (RISig LocSpecType))
hm) [DataConP]
cls [CoreBind]
cbs
= [(Var
x, Maybe LocSpecType -> Maybe LocSpecType -> MethodType LocSpecType
forall t. Maybe t -> Maybe t -> MethodType t
MT (Bool -> Var -> LocSpecType -> LocSpecType
addCC Bool
allowTC Var
x (LocSpecType -> LocSpecType)
-> (RISig LocSpecType -> LocSpecType)
-> RISig LocSpecType
-> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RISig LocSpecType -> LocSpecType
forall a. RISig a -> a
fromRISig (RISig LocSpecType -> LocSpecType)
-> Maybe (RISig LocSpecType) -> Maybe LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var
-> Var
-> HashMap Var (HashMap Symbol (RISig LocSpecType))
-> Maybe (RISig LocSpecType)
forall {t} {k} {a}.
(NamedThing t, Hashable k) =>
k -> t -> HashMap k (HashMap Symbol a) -> Maybe a
methodType Var
d Var
x HashMap Var (HashMap Symbol (RISig LocSpecType))
hm) (Bool -> Var -> LocSpecType -> LocSpecType
addCC Bool
allowTC Var
x (LocSpecType -> LocSpecType)
-> Maybe LocSpecType -> Maybe LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Var, [Type], [Var]) -> Var -> Maybe LocSpecType
forall {t} {c}.
NamedThing t =>
Maybe (Var, [Type], c) -> t -> Maybe LocSpecType
classType (CoreExpr -> Maybe (Var, [Type], [Var])
splitDictionary CoreExpr
e) Var
x)) | (Var
d,CoreExpr
e) <- [(Var, CoreExpr)]
ds, Var
x <- CoreExpr -> [Var]
grepMethods CoreExpr
e]
where
grepMethods :: CoreExpr -> [Var]
grepMethods = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod ([Var] -> [Var]) -> (CoreExpr -> [Var]) -> CoreExpr -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Var -> CoreExpr -> [Var]
forall a. CBVisitable a => HashSet Var -> a -> [Var]
freeVars HashSet Var
forall a. Monoid a => a
mempty
ds :: [(Var, CoreExpr)]
ds = ((Var, CoreExpr) -> Bool) -> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isDictionary (Var -> Bool)
-> ((Var, CoreExpr) -> Var) -> (Var, CoreExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst) ((CoreBind -> [(Var, CoreExpr)]) -> [CoreBind] -> [(Var, CoreExpr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [(Var, CoreExpr)]
forall {b}. Bind b -> [(b, Expr b)]
unRec [CoreBind]
cbs)
unRec :: Bind b -> [(b, Expr b)]
unRec (Ghc.Rec [(b, Expr b)]
xes) = [(b, Expr b)]
xes
unRec (Ghc.NonRec b
x Expr b
e) = [(b
x,Expr b
e)]
classType :: Maybe (Var, [Type], c) -> t -> Maybe LocSpecType
classType Maybe (Var, [Type], c)
Nothing t
_ = Maybe LocSpecType
forall a. Maybe a
Nothing
classType (Just (Var
d, [Type]
ts, c
_)) t
x =
case (DataConP -> Bool) -> [DataConP] -> [DataConP]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
==Var
d) (Var -> Bool) -> (DataConP -> Var) -> DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
Ghc.dataConWorkId (DataCon -> Var) -> (DataConP -> DataCon) -> DataConP -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon) [DataConP]
cls of
(DataConP
di:[DataConP]
_) ->
(DataConP -> SourcePos
dcpLoc DataConP
di SourcePos -> SpecType -> LocSpecType
forall l b. Loc l => l -> b -> Located b
`F.atLoc`) (SpecType -> LocSpecType)
-> (SpecType -> SpecType) -> SpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTyVar, Type)] -> SpecType -> SpecType
forall {r}.
(Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r) =>
[(RTyVar, Type)] -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
subst ([RTyVar] -> [Type] -> [(RTyVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (DataConP -> [RTyVar]
dcpFreeTyVars DataConP
di) [Type]
ts) (SpecType -> LocSpecType) -> Maybe SpecType -> Maybe LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Symbol -> [(Symbol, SpecType)] -> Maybe SpecType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup (t -> Symbol
forall {t}. NamedThing t => t -> Symbol
mkSymbol t
x) (((LHName, SpecType) -> (Symbol, SpecType))
-> [(LHName, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map ((LHName -> Symbol) -> (LHName, SpecType) -> (Symbol, SpecType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first LHName -> Symbol
lhNameToResolvedSymbol) ([(LHName, SpecType)] -> [(Symbol, SpecType)])
-> [(LHName, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> a -> b
$ DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
di)
[DataConP]
_ -> Maybe LocSpecType
forall a. Maybe a
Nothing
methodType :: k -> t -> HashMap k (HashMap Symbol a) -> Maybe a
methodType k
d t
x HashMap k (HashMap Symbol a)
m = Maybe (HashMap Symbol a) -> t -> Maybe a
forall {t} {a}.
NamedThing t =>
Maybe (HashMap Symbol a) -> t -> Maybe a
ihastype (k -> HashMap k (HashMap Symbol a) -> Maybe (HashMap Symbol a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup k
d HashMap k (HashMap Symbol a)
m) t
x
ihastype :: Maybe (HashMap Symbol a) -> t -> Maybe a
ihastype Maybe (HashMap Symbol a)
Nothing t
_ = Maybe a
forall a. Maybe a
Nothing
ihastype (Just HashMap Symbol a
xts) t
x = Symbol -> HashMap Symbol a -> Maybe a
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (t -> Symbol
forall {t}. NamedThing t => t -> Symbol
mkSymbol t
x) HashMap Symbol a
xts
mkSymbol :: t -> Symbol
mkSymbol t
x = Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ t -> Symbol
forall {t}. NamedThing t => t -> Symbol
GM.simplesymbol t
x
subst :: [(RTyVar, Type)] -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
subst [] RType RTyCon RTyVar r
t = RType RTyCon RTyVar r
t
subst ((RTyVar
a,Type
ta):[(RTyVar, Type)]
su) RType RTyCon RTyVar r
t = (RTyVar, RType RTyCon RTyVar r)
-> RType RTyCon RTyVar r -> RType RTyCon RTyVar 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 ()))) =>
(tv, RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarMeet' (RTyVar
a,Type -> RType RTyCon RTyVar r
forall r. Monoid r => Type -> RRType r
ofType Type
ta) ([(RTyVar, Type)] -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
subst [(RTyVar, Type)]
su RType RTyCon RTyVar r
t)
addCC :: Bool -> Ghc.Var -> LocSpecType -> LocSpecType
addCC :: Bool -> Var -> LocSpecType -> LocSpecType
addCC Bool
allowTC Var
var zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
= SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
(SpecType -> LocSpecType)
-> (SpecType -> SpecType) -> SpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType -> SpecType
forall {r}.
RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall SpecType
hst
(SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVarV Symbol (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow [] [PVarV Symbol (RType RTyCon RTyVar ())]
ps' []
(SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, SpecType)] -> SpecType -> SpecType
forall {t :: * -> *} {r} {v} {c} {tv}.
(Foldable t, Monoid r) =>
t (Symbol, RTypeV v c tv r) -> RTypeV v c tv r -> RTypeV v c tv r
makeCls [(Symbol, SpecType)]
cs'
(SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr -> Expr) -> SpecType -> SpecType
forall c tv.
(Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft (\Symbol
_ -> CoSub -> Expr -> Expr
F.applyCoSub CoSub
coSub)
(SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTyVar, RTyVar)] -> SpecType -> SpecType
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su
(SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ SpecType
st
where
hst :: SpecType
hst = Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType
t0 :: Type
t0 = Var -> Type
Ghc.varType Var
var
tyvsmap :: [(Var, RTyVar)]
tyvsmap = case Bool
-> Type
-> SpecType
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
Bare.runMapTyVars Bool
allowTC Type
t0 SpecType
st Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err of
Left Error
e -> Error -> [(Var, RTyVar)]
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw Error
e
Right MapTyVarST
s -> MapTyVarST -> [(Var, RTyVar)]
Bare.vmap MapTyVarST
s
su :: [(RTyVar, RTyVar)]
su = [(RTyVar
y, Var -> RTyVar
rTyVar Var
x) | (Var
x, RTyVar
y) <- [(Var, RTyVar)]
tyvsmap]
su' :: [(RTyVar, RType RTyCon RTyVar ())]
su' = [(RTyVar
y, RTyVar -> () -> RType RTyCon RTyVar ()
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar (Var -> RTyVar
rTyVar Var
x) ()) | (Var
x, RTyVar
y) <- [(Var, RTyVar)]
tyvsmap] :: [(RTyVar, RSort)]
coSub :: CoSub
coSub = [(Symbol, Sort)] -> CoSub
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
y, Symbol -> Sort
F.FObj (RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
x)) | (RTyVar
y, RTyVar
x) <- [(RTyVar, RTyVar)]
su]
ps' :: [PVarV Symbol (RType RTyCon RTyVar ())]
ps' = (RType RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> PVarV Symbol (RType RTyCon RTyVar ())
-> PVarV Symbol (RType RTyCon RTyVar ())
forall a b. (a -> b) -> PVarV Symbol a -> PVarV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(RTyVar, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RType RTyCon RTyVar ())]
su') (PVarV Symbol (RType RTyCon RTyVar ())
-> PVarV Symbol (RType RTyCon RTyVar ()))
-> [PVarV Symbol (RType RTyCon RTyVar ())]
-> [PVarV Symbol (RType RTyCon RTyVar ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVarV Symbol (RType RTyCon RTyVar ())]
ps
cs' :: [(Symbol, SpecType)]
cs' = [(Symbol
F.dummySymbol, RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp RTyCon
c [SpecType]
ts [] RReft
forall a. Monoid a => a
mempty) | (RTyCon
c, [SpecType]
ts) <- [(RTyCon, [SpecType])]
cs ]
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVarV Symbol (RType RTyCon RTyVar ())]
_,[(RTyCon, [SpecType])]
cs,SpecType
_) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])],
SpecType)
bkUnivClass (String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"hs-spec" (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVarV Symbol (RType RTyCon RTyVar ())]
ps,[(RTyCon, [SpecType])]
_ ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])],
SpecType)
bkUnivClass (String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"lq-spec" SpecType
st0)
makeCls :: t (Symbol, RTypeV v c tv r) -> RTypeV v c tv r -> RTypeV v c tv r
makeCls t (Symbol, RTypeV v c tv r)
c RTypeV v c tv r
t = ((Symbol, RTypeV v c tv r) -> RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> t (Symbol, RTypeV v c tv r)
-> RTypeV v c tv r
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r)
-> (Symbol, RTypeV v c tv r) -> RTypeV v c tv r -> RTypeV v c tv r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
forall r v c tv.
Monoid r =>
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun) RTypeV v c tv r
t t (Symbol, RTypeV v c tv r)
c
err :: Doc -> Doc -> TError t
err Doc
hsT Doc
lqT = SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
zz) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
var)
(String -> Doc
text String
"makeMethodTypes")
(Type -> Doc
forall a. PPrint a => a -> Doc
pprint (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
t0)
(RType RTyCon RTyVar () -> Doc
forall a. PPrint a => a -> Doc
pprint (RType RTyCon RTyVar () -> Doc) -> RType RTyCon RTyVar () -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> RType RTyCon RTyVar ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort SpecType
st0)
((Doc, Doc) -> Maybe (Doc, Doc)
forall a. a -> Maybe a
Just (Doc
hsT, Doc
lqT))
(Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan Var
var)
addForall :: RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
v RTypeV Symbol RTyCon RTyVar r
t r
r) tt :: RTypeV Symbol RTyCon RTyVar r
tt@(RAllT RTVar RTyVar (RType RTyCon RTyVar ())
v' RTypeV Symbol RTyCon RTyVar r
_ r
_)
| RTVar RTyVar (RType RTyCon RTyVar ())
v RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()) -> Bool
forall a. Eq a => a -> a -> Bool
== RTVar RTyVar (RType RTyCon RTyVar ())
v'
= RTypeV Symbol RTyCon RTyVar r
tt
| Bool
otherwise
= RTVar RTyVar (RType RTyCon RTyVar ())
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar RTVar RTyVar (RType RTyCon RTyVar ())
v) (RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall RTypeV Symbol RTyCon RTyVar r
t RTypeV Symbol RTyCon RTyVar r
tt) r
r
addForall (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
v RTypeV Symbol RTyCon RTyVar r
t r
r) RTypeV Symbol RTyCon RTyVar r
t'
= RTVar RTyVar (RType RTyCon RTyVar ())
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar RTVar RTyVar (RType RTyCon RTyVar ())
v) (RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall RTypeV Symbol RTyCon RTyVar r
t RTypeV Symbol RTyCon RTyVar r
t') r
r
addForall (RAllP PVarV Symbol (RType RTyCon RTyVar ())
_ RTypeV Symbol RTyCon RTyVar r
t) RTypeV Symbol RTyCon RTyVar r
t'
= RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall RTypeV Symbol RTyCon RTyVar r
t RTypeV Symbol RTyCon RTyVar r
t'
addForall RTypeV Symbol RTyCon RTyVar r
_ (RAllP PVarV Symbol (RType RTyCon RTyVar ())
p RTypeV Symbol RTyCon RTyVar r
t')
= PVarV Symbol (RType RTyCon RTyVar ())
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP ((RType RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> PVarV Symbol (RType RTyCon RTyVar ())
-> PVarV Symbol (RType RTyCon RTyVar ())
forall a b. (a -> b) -> PVarV Symbol a -> PVarV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(RTyVar, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RType RTyCon RTyVar ())]
su') PVarV Symbol (RType RTyCon RTyVar ())
p) RTypeV Symbol RTyCon RTyVar r
t'
addForall (RFun Symbol
_ RFInfo
_ RTypeV Symbol RTyCon RTyVar r
t1 RTypeV Symbol RTyCon RTyVar r
t2 r
_) (RFun Symbol
x RFInfo
i RTypeV Symbol RTyCon RTyVar r
t1' RTypeV Symbol RTyCon RTyVar r
t2' r
r)
= Symbol
-> RFInfo
-> RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r
-> r
-> RTypeV Symbol RTyCon RTyVar r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i (RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall RTypeV Symbol RTyCon RTyVar r
t1 RTypeV Symbol RTyCon RTyVar r
t1') (RTypeV Symbol RTyCon RTyVar r
-> RTypeV Symbol RTyCon RTyVar r -> RTypeV Symbol RTyCon RTyVar r
addForall RTypeV Symbol RTyCon RTyVar r
t2 RTypeV Symbol RTyCon RTyVar r
t2') r
r
addForall RTypeV Symbol RTyCon RTyVar r
_ RTypeV Symbol RTyCon RTyVar r
t
= RTypeV Symbol RTyCon RTyVar r
t
splitDictionary :: Ghc.CoreExpr -> Maybe (Ghc.Var, [Ghc.Type], [Ghc.Var])
splitDictionary :: CoreExpr -> Maybe (Var, [Type], [Var])
splitDictionary = [Type] -> [Var] -> CoreExpr -> Maybe (Var, [Type], [Var])
forall {b}. [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go [] []
where
go :: [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go [Type]
ts [Var]
xs (Ghc.App Expr b
e (Ghc.Tick CoreTickish
_ Expr b
a)) = [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go [Type]
ts [Var]
xs (Expr b -> Expr b -> Expr b
forall b. Expr b -> Expr b -> Expr b
Ghc.App Expr b
e Expr b
a)
go [Type]
ts [Var]
xs (Ghc.App Expr b
e (Ghc.Type Type
t)) = [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go (Type
tType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
ts) [Var]
xs Expr b
e
go [Type]
ts [Var]
xs (Ghc.App Expr b
e (Ghc.Var Var
x)) = [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go [Type]
ts (Var
xVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
xs) Expr b
e
go [Type]
ts [Var]
xs (Ghc.Tick CoreTickish
_ Expr b
t) = [Type] -> [Var] -> Expr b -> Maybe (Var, [Type], [Var])
go [Type]
ts [Var]
xs Expr b
t
go [Type]
ts [Var]
xs (Ghc.Var Var
x) = (Var, [Type], [Var]) -> Maybe (Var, [Type], [Var])
forall a. a -> Maybe a
Just (Var
x, [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
ts, [Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
xs)
go [Type]
_ [Var]
_ Expr b
_ = Maybe (Var, [Type], [Var])
forall a. Maybe a
Nothing
makeClasses :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs
-> Bare.Lookup ([DataConP], [(ModName, Ghc.Var, LocSpecType)])
makeClasses :: Env
-> SigEnv
-> ModName
-> ModSpecs
-> Lookup ([DataConP], [(ModName, Var, LocSpecType)])
makeClasses Env
env SigEnv
sigEnv ModName
myName ModSpecs
specs = do
mbZs <- [(ModName, RClass (Located BareType), TyCon)]
-> ((ModName, RClass (Located BareType), TyCon)
-> Either
[Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)])))
-> Either [Error] [Maybe (DataConP, [(ModName, Var, LocSpecType)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, RClass (Located BareType), TyCon)]
classTcs (((ModName, RClass (Located BareType), TyCon)
-> Either
[Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)])))
-> Either
[Error] [Maybe (DataConP, [(ModName, Var, LocSpecType)])])
-> ((ModName, RClass (Located BareType), TyCon)
-> Either
[Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)])))
-> Either [Error] [Maybe (DataConP, [(ModName, Var, LocSpecType)])]
forall a b. (a -> b) -> a -> b
$ \(ModName
name, RClass (Located BareType)
cls, TyCon
tc) ->
Env
-> SigEnv
-> ModName
-> ModName
-> RClass (Located BareType)
-> TyCon
-> Either [Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)]))
mkClass Env
env SigEnv
sigEnv ModName
myName ModName
name RClass (Located BareType)
cls TyCon
tc
return . second mconcat . unzip . Mb.catMaybes $ mbZs
where
classTcs :: [(ModName, RClass (Located BareType), TyCon)]
classTcs = [ (ModName
name, RClass (Located BareType)
cls, TyCon
tc) | (ModName
name, BareSpec
spec) <- ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
specs
, RClass (Located BareType)
cls <- BareSpec -> [RClass (Located BareType)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
Ms.classes BareSpec
spec
, TyCon
tc <- Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
Mb.maybeToList (RClass (Located BareType) -> Maybe TyCon
forall {ty}. RClass ty -> Maybe TyCon
classTc RClass (Located BareType)
cls) ]
classTc :: RClass ty -> Maybe TyCon
classTc = ([Error] -> Maybe TyCon)
-> (TyCon -> Maybe TyCon) -> Either [Error] TyCon -> Maybe TyCon
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe TyCon -> [Error] -> Maybe TyCon
forall a b. a -> b -> a
const Maybe TyCon
forall a. Maybe a
Nothing) TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (Either [Error] TyCon -> Maybe TyCon)
-> (RClass ty -> Either [Error] TyCon) -> RClass ty -> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) (Located LHName -> Either [Error] TyCon)
-> (RClass ty -> Located LHName)
-> RClass ty
-> Either [Error] TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BTyCon -> Located LHName
btc_tc (BTyCon -> Located LHName)
-> (RClass ty -> BTyCon) -> RClass ty -> Located LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RClass ty -> BTyCon
forall ty. RClass ty -> BTyCon
rcName
mkClass :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> RClass LocBareType -> Ghc.TyCon
-> Bare.Lookup (Maybe (DataConP, [(ModName, Ghc.Var, LocSpecType)]))
mkClass :: Env
-> SigEnv
-> ModName
-> ModName
-> RClass (Located BareType)
-> TyCon
-> Either [Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)]))
mkClass Env
env SigEnv
sigEnv ModName
_myName ModName
name (RClass BTyCon
cc [Located BareType]
ss [BTyVar]
as [(Located LHName, Located BareType)]
ms)
= Env
-> ModName
-> Either [Error] (DataConP, [(ModName, Var, LocSpecType)])
-> Either [Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)]))
forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
Bare.failMaybe Env
env ModName
name
(Either [Error] (DataConP, [(ModName, Var, LocSpecType)])
-> Either
[Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)])))
-> (TyCon
-> Either [Error] (DataConP, [(ModName, Var, LocSpecType)]))
-> TyCon
-> Either [Error] (Maybe (DataConP, [(ModName, Var, LocSpecType)]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> ModName
-> RClass (Located BareType)
-> TyCon
-> Either [Error] (DataConP, [(ModName, Var, LocSpecType)])
mkClassE Env
env SigEnv
sigEnv ModName
_myName ModName
name (BTyCon
-> [Located BareType]
-> [BTyVar]
-> [(Located LHName, Located BareType)]
-> RClass (Located BareType)
forall ty.
BTyCon -> [ty] -> [BTyVar] -> [(Located LHName, ty)] -> RClass ty
RClass BTyCon
cc [Located BareType]
ss [BTyVar]
as [(Located LHName, Located BareType)]
ms)
mkClassE :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> RClass LocBareType -> Ghc.TyCon
-> Bare.Lookup (DataConP, [(ModName, Ghc.Var, LocSpecType)])
mkClassE :: Env
-> SigEnv
-> ModName
-> ModName
-> RClass (Located BareType)
-> TyCon
-> Either [Error] (DataConP, [(ModName, Var, LocSpecType)])
mkClassE Env
env SigEnv
sigEnv ModName
_myName ModName
name (RClass BTyCon
cc [Located BareType]
ss [BTyVar]
as [(Located LHName, Located BareType)]
ms) TyCon
tc = do
ss' <- (Located BareType -> Either [Error] LocSpecType)
-> [Located BareType] -> Either [Error] [LocSpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> SigEnv
-> ModName
-> Located BareType
-> Either [Error] LocSpecType
mkConstr Env
env SigEnv
sigEnv ModName
name) [Located BareType]
ss
meths <- mapM (makeMethod env sigEnv name) ms'
let vts = [ (ModName
m, Var
v, LocSpecType
t) | (ModName
m, PlugTV Var
kv, LocSpecType
t) <- [(ModName, PlugTV Var, LocSpecType)]
meths, Var
v <- Maybe Var -> [Var]
forall a. Maybe a -> [a]
Mb.maybeToList (PlugTV Var -> Maybe Var
forall v. PlugTV v -> Maybe v
plugSrc PlugTV Var
kv) ]
let sts = [(Located LHName -> LHName
forall a. Located a -> a
val Located LHName
s, SpecType -> SpecType
unClass (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t) | (Located LHName
s, Located BareType
_) <- [(Located LHName, Located BareType)]
ms | (ModName
_, PlugTV Var
_, LocSpecType
t) <- [(ModName, PlugTV Var, LocSpecType)]
meths]
let dcp = SourcePos
-> DataCon
-> [RTyVar]
-> [PVarV Symbol (RType RTyCon RTyVar ())]
-> [SpecType]
-> [(LHName, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l DataCon
dc [RTyVar]
αs [] (LocSpecType -> SpecType
forall a. Located a -> a
val (LocSpecType -> SpecType) -> [LocSpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType]
ss') ([(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse [(LHName, SpecType)]
sts) SpecType
rt Bool
False (ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name) SourcePos
l'
return $ F.notracepp msg (dcp, vts)
where
c :: Located LHName
c = BTyCon -> Located LHName
btc_tc BTyCon
cc
l :: SourcePos
l = Located LHName -> SourcePos
forall a. Located a -> SourcePos
loc Located LHName
c
l' :: SourcePos
l' = Located LHName -> SourcePos
forall a. Located a -> SourcePos
locE Located LHName
c
msg :: String
msg = String
"MKCLASS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (BTyCon, [BTyVar], [RTyVar]) -> String
forall a. PPrint a => a -> String
F.showpp (BTyCon
cc, [BTyVar]
as, [RTyVar]
αs)
(DataCon
dc:[DataCon]
_) = TyCon -> [DataCon]
Ghc.tyConDataCons TyCon
tc
αs :: [RTyVar]
αs = BTyVar -> RTyVar
bareRTyVar (BTyVar -> RTyVar) -> [BTyVar] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BTyVar]
as
as' :: [RType c RTyVar RReft]
as' = [Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RType c RTyVar RReft) -> Var -> RType c RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Symbol -> Var
GM.symbolTyVar (Symbol -> Var) -> Symbol -> Var
forall a b. (a -> b) -> a -> b
$ BTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
a | BTyVar
a <- [BTyVar]
as ]
ms' :: [(Located LHName, Located BareType)]
ms' = [ (Located LHName
s, Symbol -> BareType -> BareType -> BareType
forall r v c tv.
Monoid r =>
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun Symbol
"" (BTyCon
-> [BareType]
-> [RTPropV Symbol BTyCon BTyVar RReft]
-> RReft
-> BareType
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp BTyCon
cc ((BTyVar -> RReft -> BareType) -> RReft -> BTyVar -> BareType
forall a b c. (a -> b -> c) -> b -> a -> c
flip BTyVar -> RReft -> BareType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RReft
forall a. Monoid a => a
mempty (BTyVar -> BareType) -> [BTyVar] -> [BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BTyVar]
as) [] RReft
forall a. Monoid a => a
mempty) (BareType -> BareType) -> Located BareType -> Located BareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareType
t) | (Located LHName
s, Located BareType
t) <- [(Located LHName, Located BareType)]
ms]
rt :: SpecType
rt = TyCon -> [SpecType] -> SpecType
forall r tv.
Monoid r =>
TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rCls TyCon
tc [SpecType]
forall {c}. [RType c RTyVar RReft]
as'
mkConstr :: Bare.Env -> Bare.SigEnv -> ModName -> LocBareType -> Bare.Lookup LocSpecType
mkConstr :: Env
-> SigEnv
-> ModName
-> Located BareType
-> Either [Error] LocSpecType
mkConstr Env
env SigEnv
sigEnv ModName
name = (LocSpecType -> LocSpecType)
-> Either [Error] LocSpecType -> Either [Error] LocSpecType
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
dropUniv) (Either [Error] LocSpecType -> Either [Error] LocSpecType)
-> (Located BareType -> Either [Error] LocSpecType)
-> Located BareType
-> Either [Error] LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> Either [Error] LocSpecType
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV
unClass :: SpecType -> SpecType
unClass :: SpecType -> SpecType
unClass = ([(RTyCon, [SpecType])], SpecType) -> SpecType
forall a b. (a, b) -> b
snd (([(RTyCon, [SpecType])], SpecType) -> SpecType)
-> (SpecType -> ([(RTyCon, [SpecType])], SpecType))
-> SpecType
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> ([(RTyCon, [SpecType])], SpecType)
forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass (SpecType -> ([(RTyCon, [SpecType])], SpecType))
-> (SpecType -> SpecType)
-> SpecType
-> ([(RTyCon, [SpecType])], SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
-> SpecType
forall t1 t2 t3. (t1, t2, t3) -> t3
thrd3 (([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
-> SpecType)
-> (SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], SpecType))
-> SpecType
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
[PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv
makeMethod :: Bare.Env -> Bare.SigEnv -> ModName -> (Located LHName, LocBareType)
-> Bare.Lookup (ModName, PlugTV Ghc.Var, LocSpecType)
makeMethod :: Env
-> SigEnv
-> ModName
-> (Located LHName, Located BareType)
-> Either [Error] (ModName, PlugTV Var, LocSpecType)
makeMethod Env
env SigEnv
sigEnv ModName
name (Located LHName
lx, Located BareType
bt) = (ModName
name, PlugTV Var
mbV,) (LocSpecType -> (ModName, PlugTV Var, LocSpecType))
-> Either [Error] LocSpecType
-> Either [Error] (ModName, PlugTV Var, LocSpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> Either [Error] LocSpecType
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
mbV Located BareType
bt
where
mbV :: PlugTV Var
mbV = ([Error] -> PlugTV Var)
-> (Var -> PlugTV Var) -> Either [Error] Var -> PlugTV Var
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (PlugTV Var -> [Error] -> PlugTV Var
forall a b. a -> b -> a
const PlugTV Var
forall v. PlugTV v
Bare.GenTV) Var -> PlugTV Var
forall v. v -> PlugTV v
Bare.LqTV (HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env Located LHName
lx)
makeSpecDictionaries
:: Bare.Env
-> Bare.SigEnv
-> (ModName, Ms.BareSpec)
-> [(ModName, Ms.BareSpec)]
-> ([RInstance LocBareType], DEnv Ghc.Var LocSpecType)
makeSpecDictionaries :: Env
-> SigEnv
-> (ModName, BareSpec)
-> [(ModName, BareSpec)]
-> ([RInstance (Located BareType)], DEnv Var LocSpecType)
makeSpecDictionaries Env
env SigEnv
sigEnv (ModName, BareSpec)
spec0 [(ModName, BareSpec)]
specs
= let ([RInstance (Located BareType)]
instances, [(Var, HashMap Symbol (RISig LocSpecType))]
specDicts) = Env
-> SigEnv
-> (ModName, BareSpec)
-> ([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))])
makeSpecDictionary Env
env SigEnv
sigEnv (ModName, BareSpec)
spec0
in ([RInstance (Located BareType)]
instances, [(Var, HashMap Symbol (RISig LocSpecType))] -> DEnv Var LocSpecType
forall t. [(Var, HashMap Symbol (RISig t))] -> DEnv Var t
dfromList ([(Var, HashMap Symbol (RISig LocSpecType))]
-> DEnv Var LocSpecType)
-> [(Var, HashMap Symbol (RISig LocSpecType))]
-> DEnv Var LocSpecType
forall a b. (a -> b) -> a -> b
$ [(Var, HashMap Symbol (RISig LocSpecType))]
specDicts [(Var, HashMap Symbol (RISig LocSpecType))]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall a. [a] -> [a] -> [a]
++ ((ModName, BareSpec)
-> [(Var, HashMap Symbol (RISig LocSpecType))])
-> [(ModName, BareSpec)]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))])
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall a b. (a, b) -> b
snd (([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))])
-> [(Var, HashMap Symbol (RISig LocSpecType))])
-> ((ModName, BareSpec)
-> ([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))]))
-> (ModName, BareSpec)
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> (ModName, BareSpec)
-> ([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))])
makeSpecDictionary Env
env SigEnv
sigEnv) [(ModName, BareSpec)]
specs)
makeSpecDictionary :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec)
-> ([RInstance LocBareType], [(Ghc.Var, M.HashMap F.Symbol (RISig LocSpecType))])
makeSpecDictionary :: Env
-> SigEnv
-> (ModName, BareSpec)
-> ([RInstance (Located BareType)],
[(Var, HashMap Symbol (RISig LocSpecType))])
makeSpecDictionary Env
env SigEnv
sigEnv (ModName
name, BareSpec
spec) =
let instances :: [RInstance (Located BareType)]
instances = BareSpec -> [RInstance (Located BareType)]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
Ms.rinstance BareSpec
spec
resolved :: [(Var, HashMap Symbol (RISig LocSpecType))]
resolved =
Env
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
resolveDictionaries Env
env ([RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))])
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall a b. (a -> b) -> a -> b
$
(RInstance (Located BareType) -> RInstance LocSpecType)
-> [RInstance (Located BareType)] -> [RInstance LocSpecType]
forall a b. (a -> b) -> [a] -> [b]
map (Env
-> SigEnv
-> ModName
-> RInstance (Located BareType)
-> RInstance LocSpecType
makeSpecDictionaryOne Env
env SigEnv
sigEnv ModName
name) [RInstance (Located BareType)]
instances
updatedInstances :: [RInstance (Located BareType)]
updatedInstances =
[ RInstance (Located BareType)
ri { riDictName = Just $ makeGHCLHNameLocatedFromId v }
| (RInstance (Located BareType)
ri, (Var
v, HashMap Symbol (RISig LocSpecType)
_)) <- [RInstance (Located BareType)]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
-> [(RInstance (Located BareType),
(Var, HashMap Symbol (RISig LocSpecType)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [RInstance (Located BareType)]
instances [(Var, HashMap Symbol (RISig LocSpecType))]
resolved
]
in ([RInstance (Located BareType)]
updatedInstances, [(Var, HashMap Symbol (RISig LocSpecType))]
resolved)
makeSpecDictionaryOne :: Bare.Env -> Bare.SigEnv -> ModName
-> RInstance LocBareType
-> RInstance LocSpecType
makeSpecDictionaryOne :: Env
-> SigEnv
-> ModName
-> RInstance (Located BareType)
-> RInstance LocSpecType
makeSpecDictionaryOne Env
env SigEnv
sigEnv ModName
name (RI BTyCon
bt Maybe (Located LHName)
mDictName [Located BareType]
lbt [(Located LHName, RISig (Located BareType))]
xts)
= String -> RInstance LocSpecType -> RInstance LocSpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"RI" (RInstance LocSpecType -> RInstance LocSpecType)
-> RInstance LocSpecType -> RInstance LocSpecType
forall a b. (a -> b) -> a -> b
$ BTyCon
-> Maybe (Located LHName)
-> [LocSpecType]
-> [(Located LHName, RISig LocSpecType)]
-> RInstance LocSpecType
forall t.
BTyCon
-> Maybe (Located LHName)
-> [t]
-> [(Located LHName, RISig t)]
-> RInstance t
RI BTyCon
bt Maybe (Located LHName)
mDictName [LocSpecType]
ts [(Located LHName
x, RISig (Located BareType) -> RISig LocSpecType
mkLSpecIType RISig (Located BareType)
t) | (Located LHName
x, RISig (Located BareType)
t) <- [(Located LHName, RISig (Located BareType))]
xts ]
where
ts :: [LocSpecType]
ts = Located BareType -> LocSpecType
mkTy' (Located BareType -> LocSpecType)
-> [Located BareType] -> [LocSpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareType]
lbt
rts :: [RTyVar]
rts = (LocSpecType -> [RTyVar]) -> [LocSpecType] -> [RTyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SpecType -> [RTyVar]
forall {v} {tv} {b} {b}. RTypeV v tv b b -> [b]
univs (SpecType -> [RTyVar])
-> (LocSpecType -> SpecType) -> LocSpecType -> [RTyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
val) [LocSpecType]
ts
univs :: RTypeV v tv b b -> [b]
univs RTypeV v tv b b
t = (\(RTVar b
tv RTVInfo (RTypeV v tv b ())
_, b
_) -> b
tv) ((RTVar b (RTypeV v tv b ()), b) -> b)
-> [(RTVar b (RTypeV v tv b ()), b)] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RTVar b (RTypeV v tv b ()), b)]
as where ([(RTVar b (RTypeV v tv b ()), b)]
as, [PVarV v (RTypeV v tv b ())]
_, RTypeV v tv b b
_) = RTypeV v tv b b
-> ([(RTVar b (RTypeV v tv b ()), b)],
[PVarV v (RTypeV v tv b ())], RTypeV v tv b b)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
[PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv RTypeV v tv b b
t
mkTy' :: LocBareType -> LocSpecType
mkTy' :: Located BareType -> LocSpecType
mkTy' = Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
forall v. PlugTV v
Bare.GenTV
mkTy :: LocBareType -> LocSpecType
mkTy :: Located BareType -> LocSpecType
mkTy = (SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)])
-> SpecType -> SpecType
forall {t :: * -> *} {tv} {v} {c} {r}.
Foldable t =>
([(RTVar tv (RTypeV v c tv ()), r)]
-> t (RTVar tv (RTypeV v c tv ()), r))
-> RTypeV v c tv r -> RTypeV v c tv r
mapUnis [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall {s} {b}. [(RTVar RTyVar s, b)] -> [(RTVar RTyVar s, b)]
tidy) (LocSpecType -> LocSpecType)
-> (Located BareType -> LocSpecType)
-> Located BareType
-> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name
PlugTV Var
forall v. PlugTV v
Bare.GenTV
mapUnis :: ([(RTVar tv (RTypeV v c tv ()), r)]
-> t (RTVar tv (RTypeV v c tv ()), r))
-> RTypeV v c tv r -> RTypeV v c tv r
mapUnis [(RTVar tv (RTypeV v c tv ()), r)]
-> t (RTVar tv (RTypeV v c tv ()), r)
f RTypeV v c tv r
t = t (RTVar tv (RTypeV v c tv ()), r)
-> [PVarV v (RTypeV v c tv ())]
-> RTypeV v c tv r
-> RTypeV v c tv r
forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v c tv r
mkUnivs ([(RTVar tv (RTypeV v c tv ()), r)]
-> t (RTVar tv (RTypeV v c tv ()), r)
f [(RTVar tv (RTypeV v c tv ()), r)]
as) [PVarV v (RTypeV v c tv ())]
ps RTypeV v c tv r
t0 where ([(RTVar tv (RTypeV v c tv ()), r)]
as, [PVarV v (RTypeV v c tv ())]
ps, RTypeV v c tv r
t0) = RTypeV v c tv r
-> ([(RTVar tv (RTypeV v c tv ()), r)],
[PVarV v (RTypeV v c tv ())], RTypeV v c tv r)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
[PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv RTypeV v c tv r
t
tidy :: [(RTVar RTyVar s, b)] -> [(RTVar RTyVar s, b)]
tidy [(RTVar RTyVar s, b)]
vs = [(RTVar RTyVar s, b)]
l [(RTVar RTyVar s, b)]
-> [(RTVar RTyVar s, b)] -> [(RTVar RTyVar s, b)]
forall a. [a] -> [a] -> [a]
++ [(RTVar RTyVar s, b)]
r
where ([(RTVar RTyVar s, b)]
l,[(RTVar RTyVar s, b)]
r) = ((RTVar RTyVar s, b) -> Bool)
-> [(RTVar RTyVar s, b)]
-> ([(RTVar RTyVar s, b)], [(RTVar RTyVar s, b)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (\(RTVar RTyVar
tv RTVInfo s
_,b
_) -> RTyVar
tv RTyVar -> [RTyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RTyVar]
rts) [(RTVar RTyVar s, b)]
vs
mkLSpecIType :: RISig LocBareType -> RISig LocSpecType
mkLSpecIType :: RISig (Located BareType) -> RISig LocSpecType
mkLSpecIType RISig (Located BareType)
t = (Located BareType -> LocSpecType)
-> RISig (Located BareType) -> RISig LocSpecType
forall a b. (a -> b) -> RISig a -> RISig b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Located BareType -> LocSpecType
mkTy RISig (Located BareType)
t
resolveDictionaries :: Bare.Env -> [RInstance LocSpecType]
-> [(Ghc.Var, M.HashMap F.Symbol (RISig LocSpecType))]
resolveDictionaries :: Env
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
resolveDictionaries Env
env = (RInstance LocSpecType
-> (Var, HashMap Symbol (RISig LocSpecType)))
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall a b. (a -> b) -> [a] -> [b]
map ((RInstance LocSpecType
-> (Var, HashMap Symbol (RISig LocSpecType)))
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))])
-> (RInstance LocSpecType
-> (Var, HashMap Symbol (RISig LocSpecType)))
-> [RInstance LocSpecType]
-> [(Var, HashMap Symbol (RISig LocSpecType))]
forall a b. (a -> b) -> a -> b
$ \RInstance LocSpecType
ri ->
let !v :: Var
v = RInstance LocSpecType -> Var
lookupDFun RInstance LocSpecType
ri
in (Var
v, [(Symbol, RISig LocSpecType)] -> HashMap Symbol (RISig LocSpecType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, RISig LocSpecType)]
-> HashMap Symbol (RISig LocSpecType))
-> [(Symbol, RISig LocSpecType)]
-> HashMap Symbol (RISig LocSpecType)
forall a b. (a -> b) -> a -> b
$ (Located LHName -> Symbol)
-> (Located LHName, RISig LocSpecType)
-> (Symbol, RISig LocSpecType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val) ((Located LHName, RISig LocSpecType)
-> (Symbol, RISig LocSpecType))
-> [(Located LHName, RISig LocSpecType)]
-> [(Symbol, RISig LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RInstance LocSpecType -> [(Located LHName, RISig LocSpecType)]
forall t. RInstance t -> [(Located LHName, RISig t)]
risigs RInstance LocSpecType
ri)
where
lookupDFun :: RInstance LocSpecType -> Var
lookupDFun (RI BTyCon
c (Just Located LHName
ldict) [LocSpecType]
_ [(Located LHName, RISig LocSpecType)]
_) = do
case HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
Bare.lookupGhcIdLHName Env
env Located LHName
ldict of
Left [Error]
e ->
Maybe SrcSpan -> String -> Var
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan) -> Located LHName -> SrcSpan
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) (String -> Var) -> String -> Var
forall a b. (a -> b) -> a -> b
$
String
"cannot find dictionary from name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Error] -> String
forall a. Show a => a -> String
show [Error]
e
Right Var
v -> Var
v
lookupDFun (RI BTyCon
c Maybe (Located LHName)
_ [LocSpecType]
ts [(Located LHName, RISig LocSpecType)]
_) = do
let tys :: [Type]
tys = (LocSpecType -> Type) -> [LocSpecType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False (SpecType -> Type)
-> (LocSpecType -> SpecType) -> LocSpecType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
dropUniv (SpecType -> SpecType)
-> (LocSpecType -> SpecType) -> LocSpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
val) [LocSpecType]
ts
case HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
reTyLookupEnv Env
env) (BTyCon -> Located LHName
btc_tc BTyCon
c) of
Left [Error]
_ ->
Maybe SrcSpan -> String -> Var
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan) -> Located LHName -> SrcSpan
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) String
"cannot find type class"
Right TyCon
tc -> case TyCon -> Maybe Class
Ghc.tyConClass_maybe TyCon
tc of
Maybe Class
Nothing ->
Maybe SrcSpan -> String -> Var
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan) -> Located LHName -> SrcSpan
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) String
"type constructor does not refer to a type class"
Just Class
cls ->
case Bool -> InstEnvs -> Class -> [Type] -> ClsInstLookupResult
Ghc.lookupInstEnv Bool
False (Env -> InstEnvs
Bare.reInstEnvs Env
env) Class
cls [Type]
tys of
((ClsInst
clsInst, [DFunInstType]
_) : [InstMatch]
_, PotentialUnifiers
_, [InstMatch]
_) ->
ClsInst -> Var
Ghc.is_dfun ClsInst
clsInst
([], PotentialUnifiers
_, [InstMatch]
_) ->
Maybe SrcSpan -> String -> Var
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan) -> Located LHName -> SrcSpan
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) String
"cannot find class instance"
dropUniv :: SpecType -> SpecType
dropUniv :: SpecType -> SpecType
dropUniv SpecType
t = SpecType
t' where ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
_,[PVarV Symbol (RType RTyCon RTyVar ())]
_,SpecType
t') = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)],
[PVarV Symbol (RType RTyCon RTyVar ())], SpecType)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
[PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv SpecType
t
makeDefaultMethods :: Bare.Env -> [(ModName, Ghc.Var, LocSpecType)]
-> [(ModName, Ghc.Var, LocSpecType)]
makeDefaultMethods :: Env
-> [(ModName, Var, LocSpecType)] -> [(ModName, Var, LocSpecType)]
makeDefaultMethods Env
env [(ModName, Var, LocSpecType)]
mts = [ (ModName
mname, Var
dm, LocSpecType
t)
| (ModName
mname, Var
m, LocSpecType
t) <- [(ModName, Var, LocSpecType)]
mts
, Just Var
dm <- [Env -> Var -> Maybe Var
lookupDefaultVar Env
env Var
m]
]
lookupDefaultVar :: Bare.Env -> Ghc.Var -> Maybe Ghc.Var
lookupDefaultVar :: Env -> Var -> Maybe Var
lookupDefaultVar Env
env Var
v =
case Var -> IdDetails
Ghc.idDetails Var
v of
Ghc.ClassOpId Class
cls Bool
_ -> do
mdm <- Var -> [(Var, DefMethInfo)] -> Maybe DefMethInfo
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
v (Class -> [(Var, DefMethInfo)]
Ghc.classOpItems Class
cls)
(n, dmspec) <- mdm
case dmspec of
DefMethSpec Type
Ghc.VanillaDM -> case HasCallStack => Env -> Located LHName -> Either [Error] Var
Env -> Located LHName -> Either [Error] Var
lookupGhcIdLHName Env
env (Name -> Located LHName
forall a. (NamedThing a, Symbolic a) => a -> Located LHName
makeGHCLHNameLocated Name
n) of
Right Var
x -> Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x
Either [Error] Var
_ -> Maybe Var
forall a. Maybe a
Nothing
DefMethSpec Type
_ -> Maybe Var
forall a. Maybe a
Nothing
IdDetails
_ -> Maybe Var
forall a. Maybe a
Nothing