diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
index 16eb422a2..9a24d8206 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs
+++ b/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
   ]
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
index ad554e45f..fe08f4248 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/DataType.hs
+++ b/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'
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
index 8f1fcebd9..8a3b259ac 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Expand.hs
+++ b/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)
 
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
index 0ab6d1ecf..a9cb5901a 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Measure.hs
+++ b/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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
index 1e0976d2a..682ca4c3e 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Resolve.hs
+++ b/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
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
index e036e72af..7d790c196 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs
+++ b/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,11 @@ 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 $
+        map (mkLogicMap . HM.map (fmap lhNameToResolvedSymbol) . liftedDefines) $
+        HM.elems $
+        getDependencies dependencies
 
     resolveFieldLogicName n =
       case n of
@@ -257,9 +258,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 +279,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
diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs
index eb7c2f563..bbd01d49d 100644
--- a/src/Prelude_LHAssumptions.hs
+++ b/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)
diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
index 7435e5301..bc75eaa8f 100644
--- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
+++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString.hs
@@ -2308,18 +2308,18 @@ findFromEndUntil f ps@(PS x s l) =
   @-}
 
 -- // for ByteString.inits
-{-@ qualif BLenGt(v:Data.ByteString.Internal.ByteString, n:int): ((bLength v) > n)
+{-@ qualif BLenGt(v:[ByteString], n:int): ((bLength v) > n)
   @-}
 
 -- // for ByteString.concat
-{-@ qualif BLens(v:List Data.ByteString.Internal.ByteString) : (0 <= bLengths v)
+{-@ qualif BLens(v:[ByteString]) : (0 <= bLengths v)
   @-}
 
-{-@ qualif BLenLE(v:GHC.Ptr.Ptr a, bs:List Data.ByteString.Internal.ByteString): (bLengths bs <= plen v)
+{-@ qualif BLenLE(v:GHC.Ptr.Ptr a, bs:[ByteString]): (bLengths bs <= plen v)
   @-}
 
 -- // for ByteString.splitWith
-{-@ qualif SplitWith(v:List Data.ByteString.Internal.ByteString, l:int): ((bLengths v) + (len v) - 1 = l)
+{-@ qualif SplitWith(v:[ByteString], l:int): ((bLengths v) + (len v) - 1 = l)
   @-}
 
 -- // for ByteString.unfoldrN
@@ -2327,9 +2327,9 @@ findFromEndUntil f ps@(PS x s l) =
   @-}
 
 -- // for ByteString.split
-{-@ qualif BSValidOff(v:int,l:int,p:GHC.ForeignPtr.ForeignPtr a): (v + l <= fplen p)
+{-@ qualif BSValidOff(v:int,l:int,p:ForeignPtr a): (v + l <= fplen p)
   @-}
 
 
-{-@ qualif SplitLoop(v:List Data.ByteString.Internal.ByteString, l:int, n:int): ((bLengths v) + (len v) - 1 = l - n)
+{-@ qualif SplitLoop(v:[ByteString], l:int, n:int): ((bLengths v) + (len v) - 1 = l - n)
   @-}
diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs
index b57b6074f..7b0612c09 100644
--- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs
+++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs
@@ -259,30 +259,30 @@ import Foreign.ForeignPtr       (ForeignPtr, withForeignPtr)
         lbLength(v) = lbLengths(bs) + lbLength(b)
   @-}
 
-{-@ qualif ByteStringNE(v:Data.ByteString.Internal.ByteString): (bLength v) > 0 @-}
-{-@ qualif BLengthsAcc(v:List Data.ByteString.Internal.ByteString,
-                       c:Data.ByteString.Internal.ByteString,
-                       cs:List Data.ByteString.Internal.ByteString):
+{-@ qualif ByteStringNE(v:S.ByteString): (bLength v) > 0 @-}
+{-@ qualif BLengthsAcc(v:List S.ByteString,
+                       c:S.ByteString,
+                       cs:List S.ByteString):
         (bLengths v) = (bLength c) + (bLengths cs)
   @-}
 
-{-@ qualif BLengthsSum(v:List (List a), bs:List Data.ByteString.Internal.ByteString):
+{-@ qualif BLengthsSum(v:List (List a), bs:List S.ByteString):
        (sumLens v) = (bLengths bs)
   @-}
 
-{-@ qualif BLenLE(v:Data.ByteString.Internal.ByteString, n:int): (bLength v) <= n @-}
-{-@ qualif BLenEq(v:Data.ByteString.Internal.ByteString,
-                  b:Data.ByteString.Internal.ByteString):
+{-@ qualif BLenLE(v:S.ByteString, n:int): (bLength v) <= n @-}
+{-@ qualif BLenEq(v:S.ByteString,
+                  b:S.ByteString):
        (bLength v) = (bLength b)
   @-}
 
 {-@ qualif BLenAcc(v:int,
-                   b1:Data.ByteString.Internal.ByteString,
-                   b2:Data.ByteString.Internal.ByteString):
+                   b1:S.ByteString,
+                   b2:S.ByteString):
        v = (bLength b1) + (bLength b2)
   @-}
 {-@ qualif BLenAcc(v:int,
-                   b:Data.ByteString.Internal.ByteString,
+                   b:S.ByteString,
                    n:int):
        v = (bLength b) + n
   @-}
@@ -308,34 +308,34 @@ import Foreign.ForeignPtr       (ForeignPtr, withForeignPtr)
   @-}
 
 {-@ qualif Chunk(v:ByteString,
-                 sb:Data.ByteString.Internal.ByteString,
+                 sb:S.ByteString,
                  lb:ByteString):
        (lbLength v) = (bLength sb) + (lbLength lb)
   @-}
 
 --LIQUID for the myriad `comb` inner functions
 {-@ qualif LBComb(v:List ByteString,
-                  acc:List Data.ByteString.Internal.ByteString,
-                  ss:List Data.ByteString.Internal.ByteString,
+                  acc:List S.ByteString,
+                  ss:List S.ByteString,
                   cs:ByteString):
         ((lbLengths v) + (len v) - 1) = ((bLengths acc) + ((bLengths ss) + (len ss) - 1) + (lbLength cs))
   @-}
 
 {-@ qualif LBGroup(v:List ByteString,
-                   acc:List Data.ByteString.Internal.ByteString,
-                   ss:List Data.ByteString.Internal.ByteString,
+                   acc:List S.ByteString,
+                   ss:List S.ByteString,
                    cs:ByteString):
         (lbLengths v) = ((bLengths acc) + (bLengths ss) + (lbLength cs))
   @-}
 
 {-@ qualif LBLenIntersperse(v:ByteString,
-                            sb:Data.ByteString.Internal.ByteString,
+                            sb:S.ByteString,
                             lb:ByteString):
         (lbLength v) = ((bLength sb) * 2) + (lbLength lb)
  @-}
 
-{-@ qualif BLenDouble(v:Data.ByteString.Internal.ByteString,
-                      b:Data.ByteString.Internal.ByteString):
+{-@ qualif BLenDouble(v:S.ByteString,
+                      b:S.ByteString):
         (bLength v) = (bLength b) * 2
  @-}
 
@@ -346,7 +346,7 @@ import Foreign.ForeignPtr       (ForeignPtr, withForeignPtr)
 
 {-@ qualif RevChunksAcc(v:ByteString,
                         acc:ByteString,
-                        cs:List Data.ByteString.Internal.ByteString):
+                        cs:List S.ByteString):
         (lbLength v) = (lbLength acc) + (bLengths cs)
   @-}
 
@@ -356,7 +356,7 @@ import Foreign.ForeignPtr       (ForeignPtr, withForeignPtr)
         (lbLength v) = (lbLength z) + (sumLens cs)
   @-}
 {-@ qualif LBCountAcc(v:int,
-                     c:Data.ByteString.Internal.ByteString,
+                     c:S.ByteString,
                      cs:ByteString):
        v <= (bLength c) + (lbLength cs)
   @-}
diff --git a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/LazyZip.hs b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/LazyZip.hs
index 11f820c99..54705b0db 100644
--- a/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/LazyZip.hs
+++ b/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/LazyZip.hs
@@ -199,7 +199,7 @@ zipWith f (Chunk a as) (Chunk b bs) = go a as b bs (sz a as b bs) 0
 sz x xs y ys = fromIntegral (S.length x) + length xs
              + fromIntegral (S.length y) + length ys
           
-{-@ qualif ByteStringNE(v:Data.ByteString.Internal.ByteString): (bLength v) > 0 @-}
+{-@ qualif ByteStringNE(v:S.ByteString): (bLength v) > 0 @-}
 
 {- qualif LBZip(v:List a,
                  x:S.ByteString,
diff --git a/tests/pos/ListQSort_LType.hs b/tests/pos/ListQSort_LType.hs
index ca37dfb49..c5a0c6f1c 100644
--- a/tests/pos/ListQSort_LType.hs
+++ b/tests/pos/ListQSort_LType.hs
@@ -15,9 +15,9 @@ llen Nil         = 0
 llen (Cons x xs) = 1 + (llen xs)
 
 
-{-@ qualif ZLLen(v:ListRange.List a) : (llen(v) >= 0)@-}
+{-@ qualif ZLLen(v:List a) : (llen(v) >= 0)@-}
 
-{-@ qualif CmpLLen(v:ListRange.List a, a:ListRange.List b) : (llen v <= llen a) @-}
+{-@ qualif CmpLLen(v:List a, a:List b) : (llen v <= llen a) @-}
 
 data List a = Nil | Cons a (List a)