Resolve type constructors in qualifiers via LHNames

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -206,6 +206,7 @@ makeGhcSpec0
   -> [(ModName, Ms.BareSpec)]
   -> Ghc.TcRn (Diagnostics, GhcSpec)
 makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs = do
+  globalRdrEnv <- Ghc.tcg_rdr_env <$> Ghc.getGblEnv
   -- build up environments
   tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
   let tyi      = Bare.tcTyConMap   tycEnv
@@ -225,7 +226,7 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
   let (dg3, refl)    = withDiagnostics $ makeSpecRefl src specs env name elaboratedSig tycEnv
   let eqs            = gsHAxioms refl
   let (dg4, measEnv) = withDiagnostics $ addOpaqueReflMeas cfg tycEnv env mySpec measEnv0 specs eqs
-  let qual     = makeSpecQual cfg env tycEnv measEnv rtEnv specs
+  let qual = makeSpecQual cfg env globalRdrEnv tycEnv measEnv rtEnv mySpec iSpecs2
   let (dg5, spcVars) = withDiagnostics $ makeSpecVars cfg src mySpec env measEnv
   let (dg6, spcTerm) = withDiagnostics $ makeSpecTerm cfg     mySpec lenv env
   let sData    = makeSpecData  src env sigEnv measEnv elaboratedSig specs
@@ -473,15 +474,25 @@ resolveStringVar env name s = Bare.lookupGhcVar env name "resolve-string-var" lx
 
 
 ------------------------------------------------------------------------------------------
-makeSpecQual :: Config -> Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> BareRTEnv -> Bare.ModSpecs
-             -> GhcSpecQual
+makeSpecQual
+  :: Config
+  -> Bare.Env
+  -> Ghc.GlobalRdrEnv
+  -> Bare.TycEnv
+  -> Bare.MeasEnv
+  -> BareRTEnv
+  -> BareSpec
+  -> Bare.ModSpecs
+  -> GhcSpecQual
 ------------------------------------------------------------------------------------------
-makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
+makeSpecQual _cfg env globalRdrEnv tycEnv measEnv _rtEnv mySpec depSpecs = SpQual
   { gsQualifiers = filter okQual quals
   , gsRTAliases  = [] -- makeSpecRTAliases env rtEnv -- TODO-REBARE
   }
   where
-    quals        = concatMap (makeQualifiers env tycEnv) (M.toList specs)
+    quals =
+      makeQualifiers env globalRdrEnv tycEnv mySpec ++
+      concatMap qualifiers (M.elems depSpecs)
     -- mSyms        = F.tracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv)
     okQual q     = F.notracepp ("okQual: " ++ F.showpp q)
                    $ all (`S.member` mSyms) (F.syms q)
@@ -490,9 +501,14 @@ makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
                    ++ (fst <$> Bare.meSyms measEnv)
                    ++ (fst <$> Bare.meClassSyms measEnv)
 
-makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec F.Symbol ty) -> [F.Qualifier]
-makeQualifiers env tycEnv (modn, spec) =
-    Mb.mapMaybe (resolveQParams env tycEnv modn) $ Ms.qualifiers spec
+makeQualifiers
+  :: Bare.Env
+  -> Ghc.GlobalRdrEnv
+  -> Bare.TycEnv
+  -> Ms.Spec F.Symbol ty
+  -> [F.Qualifier]
+makeQualifiers env globalRdrEnv tycEnv spec =
+    Mb.mapMaybe (resolveQParams env globalRdrEnv tycEnv) $ Ms.qualifiers spec
 
 
 -- | @resolveQualParams@ converts the sorts of parameters from, e.g.
@@ -501,8 +517,13 @@ makeQualifiers env tycEnv (modn, spec) =
 --   It would not be required if _all_ qualifiers are scraped from
 --   function specs, but we're keeping it around for backwards compatibility.
 
-resolveQParams :: Bare.Env -> Bare.TycEnv -> ModName -> F.Qualifier -> Maybe F.Qualifier
-resolveQParams env tycEnv name q = do
+resolveQParams
+  :: Bare.Env
+  -> Ghc.GlobalRdrEnv
+  -> Bare.TycEnv
+  -> F.Qualifier
+  -> Maybe F.Qualifier
+resolveQParams env globalRdrEnv tycEnv q = do
      qps   <- mapM goQP (F.qParams q)
      return $ q { F.qParams = qps }
   where
@@ -511,15 +532,23 @@ resolveQParams env tycEnv name q = do
     go (FAbs i s)    = FAbs i <$> go s
     go (FFunc s1 s2) = FFunc  <$> go s1 <*> go s2
     go (FApp  s1 s2) = FApp   <$> go s1 <*> go s2
-    go (FTC c)       = qualifyFTycon env tycEnv name c
+    go (FTC c)       = qualifyFTycon env globalRdrEnv tycEnv c
     go s             = Just s
 
-qualifyFTycon :: Bare.Env -> Bare.TycEnv -> ModName -> F.FTycon -> Maybe F.Sort
-qualifyFTycon env tycEnv name c
+qualifyFTycon
+  :: Bare.Env
+  -> Ghc.GlobalRdrEnv
+  -> Bare.TycEnv
+  -> F.FTycon
+  -> Maybe F.Sort
+qualifyFTycon env globalRdrEnv tycEnv c
   | isPrimFTC           = Just (FTC c)
   | otherwise           = tyConSort embs . F.atLoc tcs <$> ty
   where
-    ty                  = Bare.maybeResolveSym env name "qualify-FTycon" tcs
+    ty                  = case resolveSymbolToTcName globalRdrEnv tcs of
+      Left e -> Ex.throw [e]
+      Right lhname -> either Ex.throw Just $
+                        Bare.lookupGhcTyConLHName (Bare.reTyLookupEnv env) lhname
     isPrimFTC           = F.val tcs `elem` F.prims
     tcs                 = F.fTyconSymbol c
     embs                = Bare.tcEmbs tycEnv
@@ -1028,12 +1057,12 @@ makeInvariants :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(Maybe G
 makeInvariants env sigEnv (name, spec) =
   [ (Nothing, t)
     | (_, bt) <- Ms.invariants spec
-    , Bare.knownGhcType env name bt
+    , Bare.knownGhcType env bt
     , let t = Bare.cookSpecType env sigEnv name Bare.GenTV bt
   ] ++
   concat [ (Nothing,) . makeSizeInv l <$>  ts
     | (bts, l) <- Ms.dsize spec
-    , all (Bare.knownGhcType env name) bts
+    , all (Bare.knownGhcType env) bts
     , let ts = Bare.cookSpecType env sigEnv name Bare.GenTV <$> bts
   ]
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs

@@ -589,14 +589,14 @@ ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> Maybe (Located LHName, [
             -> Bare.Lookup ( (ModName, TyConP, Maybe DataPropDecl), [Located DataConP] )
 ofBDataDecl env name (Just dd@(DataDecl tc as ps cts pos sfun pt _)) maybe_invariance_info = do
   let Loc lc lc' _ = dataNameSymbol tc
-  let πs           = Bare.ofBPVar env name pos <$> ps
+  let πs           = Bare.ofBPVar env pos <$> ps
   let αs           = RTV . GM.symbolTyVar <$> as
   let n            = length αs
   let initmap      = zip (RT.uPVar <$> πs) [0..]
   tc'             <- getDnTyCon env name tc
   cts'            <- mapM (ofBDataCtor env name lc lc' tc' αs ps πs) (Mb.fromMaybe [] cts)
   unless (checkDataDecl tc' dd) (Left [err])
-  let pd           = Bare.ofBareType env name lc (Just []) <$> F.tracepp "ofBDataDecl-prop" pt
+  let pd           = Bare.ofBareType env lc (Just []) <$> F.tracepp "ofBDataDecl-prop" pt
   let tys          = [t | dcp <- cts', (_, t) <- dcpTyArgs dcp]
   let varInfo      = L.nub $  concatMap (getPsSig initmap True) tys
   let defPs        = varSignToVariance varInfo <$> [0 .. (length πs - 1)]
@@ -652,8 +652,8 @@ ofBDataCtorTc env name l l' tc αs ps πs _ctor@(DataCtor _c as _ xts res) c' =
     , dcpLocE       = l'
     }
   where
-    ts'           = Bare.ofBareType env name l (Just ps) <$> ts
-    res'          = Bare.ofBareType env name l (Just ps) <$> res
+    ts'           = Bare.ofBareType env l (Just ps) <$> ts
+    res'          = Bare.ofBareType env l (Just ps) <$> res
     t0'           = dataConResultTy c' αs t0 res'
     _cfg          = getConfig env
     yts           = zip xs ts'

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs

@@ -478,7 +478,7 @@ cookSpecTypeE :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> Lo
               -> Bare.Lookup LocSpecType
 -----------------------------------------------------------------------------------------
 cookSpecTypeE env sigEnv name@(ModName _ _) x bt
-  = fmap f . bareSpecType env name $ bareExpandType rtEnv bt
+  = fmap f . bareSpecType env $ bareExpandType rtEnv bt
   where
     f = (if doplug || not allowTC then plugHoles allowTC sigEnv name x else id)
         . fmap (RT.addTyConInfo embs tyi)
@@ -528,8 +528,8 @@ bareExpandType = expandLoc
 specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
 specExpandType = expandLoc
 
-bareSpecType :: Bare.Env -> ModName -> LocBareType -> Bare.Lookup LocSpecType
-bareSpecType env name bt = case Bare.ofBareTypeE env name (F.loc bt) Nothing (val bt) of
+bareSpecType :: Bare.Env -> LocBareType -> Bare.Lookup LocSpecType
+bareSpecType env bt = case Bare.ofBareTypeE env (F.loc bt) Nothing (val bt) of
   Left e  -> Left e
   Right t -> Right (F.atLoc bt t)
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs

@@ -364,7 +364,7 @@ makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec)
 ----------------------------------------------------------------------------------------------
 makeMeasureSpec env sigEnv myName (name, spec)
   = mkMeasureDCon env
-  . mkMeasureSort env               name
+  . mkMeasureSort env
   . first val
   . bareMSpec     env sigEnv myName name
   $ spec
@@ -517,7 +517,7 @@ bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims oms
     rtEnv      = Bare.sigRTEnv          sigEnv
     force      = name == myName
     inScope z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) (force ||  okSort z)
-    okSort     = Bare.knownGhcType env name . msSort
+    okSort     = Bare.knownGhcType env . msSort
 
 mkMeasureDCon :: Bare.Env -> Ms.MSpec t (F.Located LHName) -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
 mkMeasureDCon env m = do
@@ -537,13 +537,13 @@ mkMeasureDCon_ m ndcs = fmap (tx . val) m
 measureCtors ::  Ms.MSpec t (F.Located LHName) -> [F.Located LHName]
 measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap
 
-mkMeasureSort :: Bare.Env -> ModName -> Ms.MSpec BareType (F.Located LHName)
+mkMeasureSort :: Bare.Env -> Ms.MSpec BareType (F.Located LHName)
               -> Ms.MSpec SpecType (F.Located LHName)
-mkMeasureSort env name (Ms.MSpec c mm cm im) =
+mkMeasureSort env (Ms.MSpec c mm cm im) =
   Ms.MSpec (map txDef <$> c) (tx <$> mm) (tx <$> cm) (tx <$> im)
     where
       ofMeaSort :: F.SourcePos -> BareType -> SpecType
-      ofMeaSort l = Bare.ofBareType env name l Nothing
+      ofMeaSort l = Bare.ofBareType env l Nothing
 
       tx :: Measure BareType ctor -> Measure SpecType ctor
       tx (M n s eqs k u) = M n (ofMeaSort l s) (txDef <$> eqs) k u where l = GM.fSourcePos n

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -399,9 +399,9 @@ lookupGhcIdLHName env lname =
 -------------------------------------------------------------------------------
 -- | Checking existence of names
 -------------------------------------------------------------------------------
-knownGhcType :: Env ->  ModName -> LocBareType -> Bool
-knownGhcType env name (F.Loc l _ t) =
-  case ofBareTypeE env name l Nothing t of
+knownGhcType :: Env -> LocBareType -> Bool
+knownGhcType env (F.Loc l _ t) =
+  case ofBareTypeE env l Nothing t of
     Left e  -> myTracepp ("knownType: " ++ F.showpp (t, e)) False
     Right _ -> True
 
@@ -666,14 +666,14 @@ maybeResolveSym env name kind x = case resolveLocSym env name kind x of
 -------------------------------------------------------------------------------
 -- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors
 -------------------------------------------------------------------------------
-ofBareType :: HasCallStack => Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
-ofBareType env name l ps t = either fail' id (ofBareTypeE env name l ps t)
+ofBareType :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
+ofBareType env l ps t = either fail' id (ofBareTypeE env l ps t)
   where
     fail'                  = Ex.throw
     -- fail                   = Misc.errorP "error-ofBareType" . F.showpp
 
-ofBareTypeE :: HasCallStack => Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
-ofBareTypeE env name l ps t = ofBRType env name (const (resolveReft l ps t)) l t
+ofBareTypeE :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
+ofBareTypeE env l ps t = ofBRType env (const (resolveReft l ps t)) l t
 
 resolveReft :: F.SourcePos -> Maybe [PVar BSort] -> BareType -> RReft -> RReft
 resolveReft l ps t
@@ -697,14 +697,14 @@ coSubReft :: F.CoSub -> F.Reft -> F.Reft
 coSubReft su (F.Reft (x, e)) = F.Reft (x, F.applyCoSub su e)
 
 
-ofBSort :: HasCallStack => Env -> ModName -> F.SourcePos -> BSort -> RSort
-ofBSort env name l t = either (Misc.errorP "error-ofBSort" . F.showpp) id (ofBSortE env name l t)
+ofBSort :: HasCallStack => Env -> F.SourcePos -> BSort -> RSort
+ofBSort env l t = either (Misc.errorP "error-ofBSort" . F.showpp) id (ofBSortE env l t)
 
-ofBSortE :: HasCallStack => Env -> ModName -> F.SourcePos -> BSort -> Lookup RSort
-ofBSortE env name l t = ofBRType env name (const id) l t
+ofBSortE :: HasCallStack => Env -> F.SourcePos -> BSort -> Lookup RSort
+ofBSortE env l t = ofBRType env (const id) l t
 
-ofBPVar :: Env -> ModName -> F.SourcePos -> BPVar -> RPVar
-ofBPVar env name l = fmap (ofBSort env name l)
+ofBPVar :: Env -> F.SourcePos -> BPVar -> RPVar
+ofBPVar env l = fmap (ofBSort env l)
 
 --------------------------------------------------------------------------------
 txParam :: F.SourcePos -> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
@@ -734,9 +734,9 @@ type Expandable r = ( PPrint r
                     , Reftable (RTProp RTyCon RTyVar r)
                     , HasCallStack)
 
-ofBRType :: (Expandable r) => Env -> ModName -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
+ofBRType :: (Expandable r) => Env -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
          -> Lookup (RRType r)
-ofBRType env name f l = go []
+ofBRType env f l = go []
   where
     goReft bs r             = return (f bs r)
     goRFun bs x i t1 t2 r  = RFun x i{permitTC = Just (typeclass (getConfig env))} <$> (rebind x <$> go bs t1) <*> go (x:bs) t2 <*> goReft bs r
@@ -748,7 +748,7 @@ ofBRType env name f l = go []
     go bs (RAllT a t r)     = RAllT a' <$> go bs t <*> goReft bs r
       where a'              = dropTyVarInfo (mapTyVarValue RT.bareRTyVar a)
     go bs (RAllP a t)       = RAllP a' <$> go bs t
-      where a'              = ofBPVar env name l a
+      where a'              = ofBPVar env l a
     go bs (RAllE x t1 t2)   = RAllE x  <$> go bs t1    <*> go bs t2
     go bs (REx x t1 t2)     = REx   x  <$> go bs t1    <*> go (x:bs) t2
     go bs (RRTy xts r o t)  = RRTy  <$> xts' <*> goReft bs r <*> pure o <*> go bs t
@@ -757,7 +757,7 @@ ofBRType env name f l = go []
     go _ (RExprArg le)      = return    $ RExprArg le
     goRef bs (RProp ss (RHole r)) = rPropP <$> mapM goSyms ss <*> goReft bs r
     goRef bs (RProp ss t)         = RProp  <$> mapM goSyms ss <*> go bs t
-    goSyms (x, t)                 = (x,) <$> ofBSortE env name l t
+    goSyms (x, t)                 = (x,) <$> ofBSortE env l t
     goRApp bs tc ts rs r          = bareTCApp <$> goReft bs r <*> lc' <*> mapM (goRef bs) rs <*> mapM (go bs) ts
       where
         lc'                    = F.atLoc lc <$> lookupGhcTyConLHName (reTyLookupEnv env) lc

liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs

@@ -49,6 +49,7 @@
 
 module Language.Haskell.Liquid.LHNameResolution
   ( resolveLHNames
+  , resolveSymbolToTcName
   , exprArg
   , fromBareSpecLHName
   , toBareSpecLHName
@@ -191,11 +192,12 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependenc
 
     -- add defines from dependencies to the logical map
     lmap =
-      foldr (\ls lmp ->
-                 lmp <> mkLogicMap (HM.map (fmap lhNameToResolvedSymbol) $ liftedDefines ls)
-            )
-            LH.listLMap $
-            (HM.elems . getDependencies) dependencies
+        (LH.listLMap <>) $
+        mconcat $
+        reverse $
+        map (mkLogicMap . HM.map (fmap lhNameToResolvedSymbol) . liftedDefines) $
+        HM.elems $
+        getDependencies dependencies
 
     resolveFieldLogicName n =
       case n of
@@ -257,9 +259,6 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependenc
                 (errResolve (nameSpaceKind ns) "Cannot resolve name" (s <$ lname))
               pure $ val lname
 
-    errResolve :: PJ.Doc -> String -> LocSymbol -> Error
-    errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg)
-
     maybeDropImported ns es
       | localNameSpace ns = filter GHC.isLocalGRE es
       | otherwise = es
@@ -281,16 +280,40 @@ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependenc
       LHLogicNameBinder -> "logic name binder"
       LHLogicName -> "logic name"
 
-    tupleArity s =
+    isDataCon s = case Text.uncons (Text.takeWhileEnd (/= '.') (symbolText s)) of
+      Just (c, _) -> Char.isUpper c || c == ':'
+      Nothing -> False
+
+tupleArity :: Symbol -> Int
+tupleArity s =
       let a = read $ drop 5 $ symbolString s
        in if a > 64 then
             error $ "tupleArity: Too large (more than 64): " ++ show a
           else
             a
 
-    isDataCon s = case Text.uncons (Text.takeWhileEnd (/= '.') (symbolText s)) of
-      Just (c, _) -> Char.isUpper c || c == ':'
-      Nothing -> False
+errResolve :: PJ.Doc -> String -> LocSymbol -> Error
+errResolve k msg lx = ErrResolve (LH.fSrcSpan lx) k (pprint (val lx)) (PJ.text msg)
+
+-- | Produces an LHName from a symbol by looking it in the rdr environment.
+resolveSymbolToTcName :: GHC.GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
+resolveSymbolToTcName globalRdrEnv lx
+    | isTuple s =
+      pure $ LHNResolved (LHRGHC $ GHC.tupleTyConName GHC.BoxedTuple (tupleArity s)) s <$ lx
+    | isList s =
+      pure $ LHNResolved (LHRGHC GHC.listTyConName) s <$ lx
+    | s == "*" =
+      pure $ LHNResolved (LHRGHC GHC.liftedTypeKindTyConName) s <$ lx
+    | otherwise =
+      case GHC.lookupGRE globalRdrEnv (mkLookupGRE LHTcName s) of
+        [e] -> Right $ LHNResolved (LHRGHC $ GHC.greName e) s <$ lx
+        [] -> Left $ errResolve "type constructor" "Cannot resolve name" lx
+        es -> Left $ ErrDupNames
+                (LH.fSrcSpan lx)
+                (pprint s)
+                (map (PJ.text . GHC.showPprUnsafe) es)
+  where
+    s = val lx
 
 -- | Resolving logic names can produce errors and new names to add to the
 -- environment. New names might be produced when encountering data constructors

src/Prelude_LHAssumptions.hs

@@ -46,8 +46,8 @@ qualif Cmp(v:a, x:a)  : (v  = x)
 qualif Cmp(v:a, x:a)  : (v != x)
 
 qualif One(v:int)     : v = 1
-qualif True1(v:GHC.Types.Bool)   : (v)
-qualif False1(v:GHC.Types.Bool)  : (~ v)
+qualif True1(v:Bool)   : (v)
+qualif False1(v:Bool)  : (~ v)
 
 //  REBARE constant papp1 : func(1, [Pred @(0); @(0); bool])
 qualif Papp(v:a, p:Pred a) : (papp1 p v)