Merge pull request #2550 from ninioArtillero/qualify-type-aliases

allow qualify type aliases

Author: facundominguez

docs/mkDocs/docs/specifications.md

@@ -377,10 +377,27 @@ see [tests/pos/Map.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develo
 
 **Syntax:** The key requirements for type aliases are:
 
-1. Type parameters are specified in **lower**case: `a`, `b`, `c` etc.
+1. Type parameters go first and are specified in **lower**case: `a`, `b`, `c` etc.
 2. Value parameters are specified in **upper**case: `X`, `Y`, `Z` etc.
 
-## Infix  Operators
+**Import/Export:** Type aliases are exported and imported according to the following:
+
+1. When importing a module, all type aliases from its transitive dependencies are brought into scope.
+2. If a module is imported qualified, its type aliases must also be referenced with a qualifier.
+3. Locally defined aliases can shadow those from dependencies that share the same unqualified name.
+   In this case, only the local alias is stored in the resulting specification.
+   This makes possible to effectively _update_ an alias definition.
+4. When imports contain aliases with identical symbols, name resolution triggers
+   an error upon ambiguous usage. Resolve this by qualifying either:
+   - The usage
+   - The import
+   - Or both
+5. When the same alias name is imported from multiple modules (with no local definition),
+   only the lexicographically last instance is exported (i.e., included in the resulting specification).
+
+See [tests/names/pos/ImportedTypeAlias.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/names/pos/ImportedTypeAlias.hs) for examples.
+
+## Infix Operators
 
 You can define infix types and logical operators in logic [Haskell's infix notation](https://www.haskell.org/onlinereport/decls.html#fixity).
 For example, if `(+++)` is defined as a measure or reflected function, you can use it infix by declaring

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

@@ -212,7 +212,11 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
   tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier
   let tyi      = Bare.tcTyConMap   tycEnv
   let sigEnv   = makeSigEnv  embs tyi (_gsExports src) rtEnv
+  -- This spec is used to add lifted measures.
   let lSpec1   = makeLiftedSpec1 cfg src tycEnv lmap mySpec1
+  -- 'mySpec' and 'specs' contain the result of the first lifting stages, see [NOTE]: REFLECT-IMPORTS
+  -- and the expanded aliases obtained using 'rtEnv'. 'myRTE' is a filtered 'rtEnv' used at the final
+  -- lifting.
   let mySpec   = mySpec2 <> lSpec1
   let specs    = M.insert name mySpec iSpecs2
   let myRTE    = myRTEnv       src env sigEnv rtEnv
@@ -287,10 +291,26 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
                 , privateReflects = mconcat $ map (privateReflects . snd) mspecs
                 , defines = Ms.defines targetSpec
                 , usedDataCons = usedDcs
+                  -- Placing the targetSpec at the end causes local type aliases
+                  -- to take precedence over imported ones when their names clash.
+                  -- Alternatively, the last among dependencySpecs (which is
+                  -- ordered lexcographically) is picked.
+                  -- See @tests/name/pos/ImportedTypeAlias.hs@
+                , aliases = M.elems $ M.fromList $
+                    [ (lhNameToUnqualifiedSymbol (val . rtName $ rt) , rt)
+                    | rt <- concat $
+                        map (aliases . snd) dependencySpecs ++
+                        [expandedTypeAliasesOf myRTE targetSpec]
+                    ]
                 }
     })
   where
     thisModule = Ghc.tcg_mod tcg
+    expandedTypeAliasesOf myRTE sp =
+      Mb.mapMaybe
+      ((`M.lookup` typeAliases myRTE) . val . rtName)
+      (aliases sp)
+
     -- typeclass elaboration
 
     coreToLg ce =
@@ -322,14 +342,19 @@ makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec
     simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
     simplifier = pure -- no simplification
     allowTC  = typeclass cfg
+    -- Specs with type and expression aliases expanded.
     mySpec2  = Bare.expand rtEnv (F.dummyPos "expand-mySpec2") mySpec1
     iSpecs2  = Bare.expand rtEnv (F.dummyPos "expand-iSpecs2") (M.fromList dependencySpecs)
+    -- Environment for alias lookup and expansion.
     rtEnv    = Bare.makeRTEnv env name mySpec1 dependencySpecs lmap
     mspecs   = (name, mySpec0) : dependencySpecs
+    -- mySpec0 adds typeclass methods to the target spec.
     (mySpec0, instMethods)  = if allowTC
                               then Bare.compileClasses src env (name, targetSpec) dependencySpecs
                               else (targetSpec, [])
+    -- Ready for type alias expantion.
     mySpec1  = mySpec0 <> lSpec0
+    -- This spec just has the 'ealiases' (with Haskell inlines) and 'dataDecls' fields.
     lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0
     embs     = makeEmbeds          src ghcTyLookupEnv (mySpec0 : map snd dependencySpecs)
     dm       = Bare.tcDataConMap tycEnv0
@@ -1386,7 +1411,6 @@ makeLiftedSpec name src env refl sData sig qual myRTE lSpec0 = lSpec0
     xbs           = toBare <$> reflTySigs
     reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl]
     reflVars      = S.fromList (fst <$> reflTySigs)
-    -- myAliases fld = M.elems . fld $ myRTE
     srcF          = _giTarget src
 
     isLocalName = \case
@@ -1418,42 +1442,46 @@ locFile = Misc.fst3 . F.sourcePosElts . F.sp_start . F.srcSpan
 
 
 --------------------------------------------------------------------------------
--- | @myRTEnv@ slices out the part of RTEnv that was generated by aliases defined
---   in the _target_ file, "cooks" the aliases (by conversion to SpecType), and
---   then saves them back as BareType.
+-- | @myRTEnv@ extracts the portion of the RTEnv generated by expression
+--   aliases defined in the _target_ file, and "cooks" the type aliases
+--   by converting them to SpecType and then back to BareType.
 --------------------------------------------------------------------------------
 myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv
 myRTEnv src env sigEnv rtEnv = mkRTE tAs' eAs
   where
-    tAs'                     = normalizeBareAlias env sigEnv name <$> tAs
-    tAs                      = myAliases typeAliases
-    eAs                      = myAliases exprAliases
-    myAliases fld            = filter (isLocInFile srcF) . M.elems . fld $ rtEnv
-    srcF                     = _giTarget    src
-    name                     = _giTargetMod src
-
-mkRTE :: [Located (RTAlias x a)] -> [Located (RTAlias F.Symbol F.Expr)] -> RTEnv x a
+    tAs'          = normalizeBareAlias env sigEnv name <$> tAs
+    tAs           = myAliases typeAliases
+    eAs           = filter (isLocInFile srcF . rtName) $ myAliases exprAliases
+    myAliases fld = M.elems . fld $ rtEnv
+    srcF          = _giTarget    src
+    name          = _giTargetMod src
+
+mkRTE :: [RTAlias x a] -> [RTAlias F.Symbol F.Expr] -> RTEnv x a
 mkRTE tAs eAs   = RTE
   { typeAliases = M.fromList [ (aName a, a) | a <- tAs ]
-  , exprAliases = M.fromList [ (aName a, a) | a <- eAs ]
+  , exprAliases = M.fromList [ (lhNameToUnqualifiedSymbol $ aName a, a) | a <- eAs ]
   }
-  where aName   = rtName . F.val
+  where aName   = F.val . rtName
 
-normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias
-                   -> Located BareRTAlias
-normalizeBareAlias env sigEnv name lx = fixRTA <$> lx
+-- | Prepare an alias for constraint checking by /fixing/ its body and type argument names.
+normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> BareRTAlias
+                   -> BareRTAlias
+normalizeBareAlias env sigEnv name a = fixRTA a
   where
     fixRTA  :: BareRTAlias -> BareRTAlias
     fixRTA  = mapRTAVars fixArg . fmap fixBody
 
+    -- | Uses GHC to assign arguments a unique symbol by lifting them as local 'Type' variables and back.
     fixArg  :: Symbol -> Symbol
     fixArg  = F.symbol . GM.symbolTyVar
 
+    -- | Completely /cooks/ the body of a type alias by conversion to 'SpecType'
+    -- and back. At this point they have been expanded already.
     fixBody :: BareType -> BareType
     fixBody = Bare.specToBare
             . F.val
             . Bare.cookSpecType env sigEnv name Bare.RawTV
-            . F.atLoc lx
+            . F.atLoc (rtName a)
 
 
 withDiagnostics :: (Monoid a) => Bare.Lookup a -> (Diagnostics, a)

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

@@ -166,7 +166,7 @@ checkTargetSpec specs src env cbs tsp
                      -- TODO-REBARE ++ checkQualifiers env                                       (gsQualifiers (gsQual sp))
                      <> checkDuplicate                                            (gsAsmSigs    (gsSig tsp))
                      <> checkDupIntersect                                         (gsTySigs (gsSig tsp)) (gsAsmSigs (gsSig tsp))
-                     <> checkRTAliases "Type Alias" env            tAliases
+                     <> checkRTAliases "Type Alias" env            myTAliases
                      <> checkRTAliases "Pred Alias" env            eAliases
                      -- ++ _checkDuplicateFieldNames                   (gsDconsP sp)
                      -- NV TODO: allow instances of refined classes to be refined
@@ -181,7 +181,7 @@ checkTargetSpec specs src env cbs tsp
 
     _rClasses         = concatMap Ms.classes specs
     _rInsts           = concatMap Ms.rinstance specs
-    tAliases          = concat [Ms.aliases sp  | sp <- specs]
+    myTAliases        = Ms.aliases (head specs) -- We check for duplicate aliases within the target spec only.
     eAliases          = concat [Ms.ealiases sp | sp <- specs]
     emb              = gsTcEmbeds (gsName tsp)
     tcEnv            = gsTyconEnv (gsName tsp)
@@ -363,7 +363,7 @@ checkIAlOne allowHO bsc emb tcEnv env (t1, t2) =
 
 
 -- FIXME: Should _ be removed if it isn't used?
-checkRTAliases :: String -> t -> [Located (RTAlias s a)] -> Diagnostics
+checkRTAliases :: String -> t -> [RTAlias s a] -> Diagnostics
 checkRTAliases msg _ as = err1s
   where
     err1s               = checkDuplicateRTAlias msg as
@@ -456,15 +456,15 @@ checkClassMethods (Just clsis) cms xts =
     xts' = F.notracepp "XTS" $ filter (not . (`elem` cls) . fst) xts
     cls  = F.notracepp "CLS" cms
 
-checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> Diagnostics
+checkDuplicateRTAlias :: String -> [RTAlias s a] -> Diagnostics
 checkDuplicateRTAlias s tas = mkDiagnostics mempty (map mkError dups)
   where
-    mkError xs@(x:_)          = ErrDupAlias (GM.fSrcSpan x)
-                                          (text s)
-                                          (pprint . rtName . val $ x)
-                                          (GM.fSrcSpan <$> xs)
-    mkError []                = panic Nothing "mkError: called on empty list"
-    dups                    = [z | z@(_:_:_) <- groupDuplicatesOn (rtName . val) tas]
+    mkError xs@(x:_) = ErrDupAlias (GM.fSrcSpan $ rtName x)
+                                   (text s)
+                                   (pprint $ rtName x)
+                                   (GM.fSrcSpan . rtName <$> xs)
+    mkError []       = panic Nothing "mkError: called on empty list"
+    dups             = [z | z@(_:_:_) <- groupDuplicatesOn (lhNameToUnqualifiedSymbol . val . rtName) tas]
 
 groupDuplicatesOn :: Ord b => (a -> b) -> [a] -> [[a]]
 groupDuplicatesOn f = L.groupBy ((==) `on` f) . L.sortOn f
@@ -777,6 +777,3 @@ checkClassMeasures measures = mkDiagnostics mempty (mapMaybe checkOne byTyCon)
                                       (pprint (val (msName m)))
                                       (pprint ((dataConTyCon . ctor . head . msEqns) m))
                                       (GM.fSrcSpan <$> (m:ms)))
-
-
-