Expand type aliases in dependent pairs

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

@@ -327,6 +327,16 @@ instance Expand BareType where
     = expandReft     rtEnv l -- apply expression aliases
     . expandBareType rtEnv l -- apply type       aliases
 
+instance Expand () where
+  expand _ _ = id
+
+instance Expand (BRType ()) where
+  expand rtEnv l
+    = expandReft     rtEnv l -- apply expression aliases
+    . void
+    . expandBareType rtEnv l -- apply type       aliases
+    . fmap (const mempty)
+
 instance Expand (RTAlias F.Symbol Expr) where
   expand rtEnv l x = x { rtBody = expand rtEnv l (rtBody x) }
 
@@ -395,7 +405,7 @@ expandBareSpec rtEnv l sp = sp
   where f      = expand rtEnv l
 
 expandBareType :: BareRTEnv -> F.SourcePos -> BareType -> BareType
-expandBareType rtEnv _ = go
+expandBareType rtEnv l = go
   where
     go (RApp c ts rs r)  = case lookupRTEnv c rtEnv of
                              Just rta -> expandRTAliasApp (GM.fSourcePos c) rta (go <$> ts) r
@@ -410,7 +420,7 @@ expandBareType rtEnv _ = go
     go t@RHole{}         = t
     go t@RVar{}          = t
     go t@RExprArg{}      = t
-    goRef (RProp ss t)   = RProp ss (go t)
+    goRef (RProp ss t)   = RProp (map (expand rtEnv l <$>) ss) (go t)
 
 lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located BareRTAlias)
 lookupRTEnv c rtEnv = M.lookup (getLHNameSymbol $ val $ btc_tc c) (typeAliases rtEnv)

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

@@ -850,13 +850,13 @@ maybeResolveSym env name kind x = case resolveLocSym env name kind x of
 -------------------------------------------------------------------------------
 -- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors
 -------------------------------------------------------------------------------
-ofBareType :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
+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)
   where
     fail'                  = Ex.throw
     -- fail                   = Misc.errorP "error-ofBareType" . F.showpp
 
-ofBareTypeE :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
+ofBareTypeE :: HasCallStack => Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
 ofBareTypeE env name l ps t = ofBRType env name (resolveReft env name l ps t) l t
 
 resolveReft :: Env -> ModName -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> [F.Symbol] -> RReft -> RReft
@@ -882,10 +882,10 @@ coSubReft :: F.CoSub -> F.Reft -> F.Reft
 coSubReft su (F.Reft (x, e)) = F.Reft (x, F.applyCoSub su e)
 
 
-ofBSort :: Env -> ModName -> F.SourcePos -> BSort -> RSort
+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)
 
-ofBSortE :: Env -> ModName -> F.SourcePos -> BSort -> Lookup RSort
+ofBSortE :: HasCallStack => Env -> ModName -> F.SourcePos -> BSort -> Lookup RSort
 ofBSortE env name l t = ofBRType env name (const id) l t
 
 ofBPVar :: Env -> ModName -> F.SourcePos -> BPVar -> RPVar
@@ -916,7 +916,8 @@ rtypePredBinds = map RT.uPVar . ty_preds . toRTypeRep
 type Expandable r = ( PPrint r
                     , Reftable r
                     , SubsTy RTyVar (RType RTyCon RTyVar ()) r
-                    , Reftable (RTProp RTyCon RTyVar r))
+                    , Reftable (RTProp RTyCon RTyVar r)
+                    , HasCallStack)
 
 ofBRType :: (Expandable r) => Env -> ModName -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
          -> Lookup (RRType r)
@@ -947,7 +948,7 @@ ofBRType env name f l = go []
         lc'                    = F.atLoc lc <$> lookupGhcTyConLHName env lc
         lc                     = btc_tc tc
 
-lookupGhcTyConLHName :: Env -> Located LHName -> Lookup Ghc.TyCon
+lookupGhcTyConLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.TyCon
 lookupGhcTyConLHName env lc = do
     case lookupTyThing env lc of
       Ghc.ATyCon tc -> Right tc
@@ -961,7 +962,7 @@ lookupGhcTyConLHName env lc = do
 -- This should be benign because the result doesn't depend of when exactly this is
 -- called. Since this code is intended to be used inside a GHC plugin, there is no
 -- danger that GHC is finalized before the result is evaluated.
-lookupTyThingMaybe :: Env -> Located LHName -> Maybe Ghc.TyThing
+lookupTyThingMaybe :: HasCallStack => Env -> Located LHName -> Maybe Ghc.TyThing
 lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
     case c0 of
       LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "unresolved name: " ++ show c0
@@ -972,7 +973,7 @@ lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
         LHRGHC n ->
           Ghc.reflectGhc (Interface.lookupTyThing (reTypeEnv env) n) (reSession env)
 
-lookupTyThing :: Env -> Located LHName -> Ghc.TyThing
+lookupTyThing :: HasCallStack => Env -> Located LHName -> Ghc.TyThing
 lookupTyThing env lc =
     Mb.fromMaybe (panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show (val lc)) $
       lookupTyThingMaybe env lc

tests/names/pos/ExpandsDependentPairs.hs

@@ -0,0 +1,12 @@
+-- | Tests that Id is correctly expanded. Before fixing, this test would
+-- fail with
+--
+-- > lookupTyThing: cannot resolve a LHRLogic name "Id"
+--
+module ExpandsDependentPairs where
+
+{-@ type Id = {v:Int | v >= 0} @-}
+
+{-@ lemma :: l:Id -> (id::Id, { true }) @-}
+lemma :: Int -> (Int, ())
+lemma x = (x, ())

tests/tests.cabal

@@ -785,6 +785,7 @@ executable names-pos
                     , Capture01
                     , Capture02
                     , ClojurVector
+                    , ExpandsDependentPairs
                     , HideName00
                     , HidePrelude
                     , List00