Retain System naems until the end of typechecking
authorRichard Eisenberg <eir@cis.upenn.edu>
Sun, 28 Jun 2015 17:53:32 +0000 (13:53 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Sun, 28 Jun 2015 17:53:32 +0000 (13:53 -0400)
compiler/basicTypes/Name.hs
compiler/basicTypes/Var.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcMType.hs

index 88b6e68..528f5af 100644 (file)
@@ -49,6 +49,7 @@ module Name (
         nameUnique, setNameUnique,
         nameOccName, nameModule, nameModule_maybe,
         setNameLoc,
+        toInternalName,
         tidyNameOcc,
         localiseName,
         mkLocalisedOccName,
@@ -365,6 +366,11 @@ setNameUnique name uniq = name {n_uniq = getKeyFastInt uniq}
 setNameLoc :: Name -> SrcSpan -> Name
 setNameLoc name loc = name {n_loc = loc}
 
+-- | Convert a name into an Internal name. Used in zonking.
+-- See Note [Visible type application] in TcExpr
+toInternalName :: Name -> Name
+toInternalName name = name { n_sort = Internal }
+
 tidyNameOcc :: Name -> OccName -> Name
 -- We set the OccName of a Name when tidying
 -- In doing so, we change System --> Internal, so that when we print
index 9827450..44d125e 100644 (file)
@@ -62,7 +62,7 @@ module Var (
 
         -- ** Modifying 'TyVar's
         setTyVarName, setTyVarUnique, setTyVarKind, updateTyVarKind,
-        updateTyVarKindM
+        updateTyVarKindM, toInternalTyVar
 
     ) where
 
@@ -290,6 +290,11 @@ updateTyVarKindM update tv
   = do { k' <- update (tyVarKind tv)
        ; return $ tv {varType = k'} }
 
+-- | Change a tyvar's name to be Internal. Used in the final zonk.
+-- See also Note [Visible type application] in TcExpr
+toInternalTyVar :: TyVar -> TyVar
+toInternalTyVar tv = setTyVarName tv (toInternalName (getName tv))
+
 mkTyVar :: Name -> Kind -> TyVar
 mkTyVar name kind = TyVar { varName    = name
                           , realUnique = getKeyFastInt (nameUnique name)
index ac36908..5e4200d 100644 (file)
@@ -10,7 +10,7 @@
 module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
                  tcHsBootSigs, tcPolyCheck,
                  PragFun, tcSpecPrags, tcSpecWrapper,
-                 tcVectDecls, 
+                 tcVectDecls,
                  TcSigInfo(..), TcSigFun, mkPragFun,
                  instTcTySig, instTcTySigFromId, findScopedTyVars,
                  badBootDeclErr, mkExport ) where
@@ -827,7 +827,7 @@ and the proof is the impedance matcher.
 Notice that the impedance matcher may do defaulting.  See Trac #7173.
 
 It also cleverly does an ambiguity check; for example, rejecting
-   f :: F a -> a
+   f :: F a -> a
 where F is a non-injective type function.
 -}
 
@@ -864,9 +864,9 @@ The basic idea is this:
    f:: Num a => a -> b -> a
    {-# SPECIALISE foo :: Int -> b -> Int #-}
 
-We check that 
-   (forall a. Num a => a -> a) 
-      is more polymorphic than 
+We check that
+   (forall a. Num a => a -> a)
+      is more polymorphic than
    Int -> Int
 (for which we could use tcSubType, but see below), generating a HsWrapper
 to connect the two, something like
@@ -912,7 +912,7 @@ From the TcSpecPrag, in DsBinds we generate a binding for f_spec and a RULE:
    RULE: forall b (d:Num b). f b d = f_spec b
 
 The RULE is generated by taking apart the HsWrapper, which is a little
-delicate, but works.  
+delicate, but works.
 
 Some wrinkles
 
@@ -949,7 +949,7 @@ Some wrinkles
           f_spec = <f rhs> Int dNumInt
 
           RULE: forall d. f Int d = f_spec
-      You can see this discarding happening in 
+      You can see this discarding happening in
 
 3. Note that the HsWrapper can transform *any* function with the right
    type prefix
@@ -1016,7 +1016,7 @@ tcSpecPrags poly_id prag_sigs
 tcSpecPrag :: TcId -> Sig Name -> TcM [TcSpecPrag]
 tcSpecPrag poly_id prag@(SpecSig fun_name hs_tys inl)
 -- See Note [Handling SPECIALISE pragmas]
--- 
+--
 -- The Name fun_name in the SpecSig may not be the same as that of the poly_id
 -- Example: SPECIALISE for a class method: the Name in the SpecSig is
 --          for the selector Id, but the poly_id is something like $cop
@@ -1044,7 +1044,7 @@ tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
 tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
 -- A simpler variant of tcSubType, used for SPECIALISE pragmas
 -- See Note [Handling SPECIALISE pragmas], wrinkle 1
-tcSpecWrapper ctxt poly_ty spec_ty 
+tcSpecWrapper ctxt poly_ty spec_ty
   = do { (sk_wrap, inst_wrap)
                <- tcGen ctxt spec_ty $ \ _ spec_tau ->
                   do { (inst_wrap, tau) <- deeplyInstantiate orig poly_ty
index 826d143..1a883db 100644 (file)
@@ -1038,6 +1038,59 @@ With the change, f1 will type-check, because the 'Char' info from
 the signature is propagated into MkQ's argument. With the check
 in the other order, the extra signature in f2 is reqd.
 
+Note [Visible type application]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+TODO (RAE): Move Note?
+
+GHC implements a generalisation of the algorithm described in the
+"Visible Type Application" paper (available from
+http://www.cis.upenn.edu/~sweirich/publications.html). A key part
+of that algorithm is to distinguish "known" variables from "unknown"
+variables. For example, the following should typecheck:
+
+  f :: forall a b. a -> b -> b
+  f = const id
+
+  g = const id
+
+  x = f @Int @Bool 5 False
+  y = g 5 @Bool False
+
+The idea is that we wish to allow visible type application when we are
+instantiating a known, fixed variable. In practice, known, fixed variables
+are either written in a user-specified type signature (or annotation), OR
+are imported from another module. (We could do better here, for example
+by doing SCC analysis on parts of a module and considering any type from
+outside one's SCC to be fully known, but this is very confusing to users.
+The simple rule above is much more straightforward and predictable.)
+
+So, both of f's quantified variables are known and may be instantiated.
+But g has no type signature, so only id's variable is known (because id
+is imported). We write the type of g as forall {a}. a -> forall b. b -> b.
+Note that the a is in braces, meaning it cannot be instantiated with
+visible type application.
+
+Tracking known vs. unknown variables is done conveniently by looking at
+Names. A System name (from mkSystemName or a variant) is an unknown
+variable; an Internal name is a known one. Simple. This works out
+because skolemiseUnboundMetaTyVar always produces a System name.
+
+The only wrinkle with this scheme is in tidying. If all inferred names
+are System names, then tidying will append lots of 0s. This pollutes
+interface files and Haddock output. So we convert System tyvars to
+Internal ones during the final zonk. This works because type-checking
+is fully complete, and therefore the distinction between known and
+unknown is no longer relevant.
+
+If using System vs. Internal to perform type-checking seems suspicious,
+the alternative approach would mean adding a field to ForAllTy to track
+known vs. unknown. That seems considerably more painful. And, anyway,
+once the (* :: *) branch is merged, this will be redesigned somewhat
+to move away from using Names. That's because the (* :: *) branch already
+has more structure available in ForAllTy, and there, it's easy to squeeze
+in another known-vs.-unknown bit.
+
+TODO (RAE): Update this Note in the (* :: *) branch when merging.
 
 ************************************************************************
 *                                                                      *
index 032a732..ff79391 100644 (file)
@@ -289,7 +289,7 @@ zonkTyBndrX :: ZonkEnv -> TyVar -> TcM (ZonkEnv, TyVar)
 -- then we add it to the envt, so all occurrences are replaced
 zonkTyBndrX env tv
   = do { ki <- zonkTcTypeToType env (tyVarKind tv)
-       ; let tv' = mkTyVar (tyVarName tv) ki
+       ; let tv' = mkTyVar (toInternalName $ tyVarName tv) ki
        ; return (extendTyZonkEnv1 env tv', tv') }
 
 zonkTopExpr :: HsExpr TcId -> TcM (HsExpr Id)
@@ -1402,7 +1402,10 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
                  ; case cts of
                       Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
                                             zonkTcTypeToType env (tyVarKind tv)
-                                  ; zonk_unbound_tyvar (setTyVarKind tv kind) }
+                                    -- See Note [Visible type application]
+                                    -- in TcExpr about the toInternalTyVar
+                                  ; zonk_unbound_tyvar (toInternalTyVar $
+                                                        setTyVarKind tv kind) }
                       Indirect ty -> do { zty <- zonkTcTypeToType env ty
                                         -- Small optimisation: shortern-out indirect steps
                                         -- so that the old type may be more easily collected.
@@ -1413,7 +1416,9 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
   where
     lookup_in_env    -- Look up in the env just as we do for Ids
       = case lookupVarEnv tv_env tv of
-          Nothing  -> return (mkTyVarTy tv)
+                        -- See Note [Visible type application]
+                        -- in TcExpr about the toInternalTyVar
+          Nothing  -> return (mkTyVarTy $ toInternalTyVar tv)
           Just tv' -> return (mkTyVarTy tv')
 
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
index 326e4bb..edb84d8 100644 (file)
@@ -580,7 +580,9 @@ skolemiseUnboundMetaTyVar tv details
               new_tv_name = if isWildcardVar tv
                             then generaliseWildcardVarName tv_name
                             else tv_name
-              final_name = mkInternalName uniq new_tv_name span
+                -- NB: make a System name. See Note [Visible type application]
+                -- in TcExpr
+              final_name = mkSystemNameAt uniq new_tv_name span
               final_kind = defaultKind kind
               final_tv   = mkTcTyVar final_name final_kind details