Allow foralls in instance decls
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 8 Feb 2016 09:05:12 +0000 (09:05 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 8 Feb 2016 09:07:07 +0000 (09:07 +0000)
This patch finally makes it possible to have explicit
foralls in an instance decl
   instance forall (a :: *). Eq a => Eq [a] where ...

This is useful to allow kind signatures or indeed
explicicit kind for-alls; see Trac #11519

I thought it would be really easy, because an instance
declaration already contains an actual HsSigType, so all
the syntactic baggage is there.  But in fact it turned
out that instance declarations were kind-checked a
little differently, because the body kind of the forall
is 'Constraint' rather than '*'.

So I fixed that.  There a slight kludge
(see Note [Body kind of a HsQualTy], but it's still a
significant improvement.

I also did the usual other round of refactoring,
improved a few error messages, tidied up comments etc.
The only significant aspect of all that was

  * Kill mkNakedSpecSigmaTy, mkNakedPhiTy, mkNakedFunTy
    These function names suggest that they do something
    complicated, but acutally they do nothing. So I
    killed them.

  * Swap the arg order of mkNamedBinder, just so that it is
    convenient to say 'map (mkNamedBinder Invisible) tvs'

  * I had to improve isPredTy, to deal with (illegal)
    types like
       (Eq a => Eq [a]) => blah
    See Note [isPeredTy complications] in Type.hs

Still to come: user manual documentation for the
instance-decl change.

30 files changed:
compiler/hsSyn/HsTypes.hs
compiler/hsSyn/HsUtils.hs
compiler/rename/RnSource.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs
testsuite/tests/gadt/T3163.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr
testsuite/tests/indexed-types/should_fail/T10899.stderr
testsuite/tests/indexed-types/should_fail/T9357.stderr
testsuite/tests/rename/should_fail/rnfail026.stderr
testsuite/tests/typecheck/should_fail/T11355.stderr
testsuite/tests/typecheck/should_fail/T2538.stderr
testsuite/tests/typecheck/should_fail/T5957.stderr
testsuite/tests/typecheck/should_fail/T7019.stderr
testsuite/tests/typecheck/should_fail/T7019a.stderr
testsuite/tests/typecheck/should_fail/T7809.stderr
testsuite/tests/typecheck/should_fail/T8806.stderr
testsuite/tests/typecheck/should_fail/T9196.stderr
testsuite/tests/typecheck/should_fail/tcfail088.stderr
testsuite/tests/typecheck/should_fail/tcfail127.stderr
testsuite/tests/typecheck/should_fail/tcfail184.stderr
testsuite/tests/typecheck/should_fail/tcfail195.stderr
testsuite/tests/typecheck/should_fail/tcfail196.stderr
testsuite/tests/typecheck/should_fail/tcfail197.stderr

index 15de6a0..a14c24d 100644 (file)
@@ -53,11 +53,12 @@ module HsTypes (
         hsScopedTvs, hsWcScopedTvs, dropWildCards,
         hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
         hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
-        splitLHsInstDeclTy,
+        splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
         splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
-        splitHsFunType, splitHsAppTys,
-        mkHsOpTy,
+        splitHsFunType, splitHsAppsTy,
+        splitHsAppTys, getAppsTyHead_maybe, hsTyGetAppHead_maybe,
+        mkHsOpTy, mkHsAppTy, mkHsAppTys,
         ignoreParens, hsSigType, hsSigWcType,
         hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
 
@@ -569,9 +570,6 @@ data HsTyLit
   | HsStrTy SourceText FastString
     deriving (Data, Typeable)
 
-mkHsOpTy :: LHsType name -> Located name -> LHsType name -> HsType name
-mkHsOpTy ty1 op ty2 = HsOpTy ty1 op ty2
-
 newtype HsWildCardInfo name      -- See Note [The wildcard story for types]
     = AnonWildCard (PostRn name (Located Name))
       -- A anonymous wild card ('_'). A fresh Name is generated for
@@ -737,71 +735,6 @@ instance (Outputable arg, Outputable rec)
   ppr (RecCon rec)     = text "RecCon:" <+> ppr rec
   ppr (InfixCon l r)   = text "InfixCon:" <+> ppr [l, r]
 
-type LFieldOcc name = Located (FieldOcc name)
-
--- | Represents an *occurrence* of an unambiguous field.  We store
--- both the 'RdrName' the user originally wrote, and after the
--- renamer, the selector function.
-data FieldOcc name = FieldOcc { rdrNameFieldOcc  :: Located RdrName
-                                 -- ^ See Note [Located RdrNames] in HsExpr
-                              , selectorFieldOcc :: PostRn name name
-                              }
-  deriving Typeable
-deriving instance Eq (PostRn name name) => Eq (FieldOcc name)
-deriving instance Ord (PostRn name name) => Ord (FieldOcc name)
-deriving instance (Data name, Data (PostRn name name)) => Data (FieldOcc name)
-
-instance Outputable (FieldOcc name) where
-  ppr = ppr . rdrNameFieldOcc
-
-mkFieldOcc :: Located RdrName -> FieldOcc RdrName
-mkFieldOcc rdr = FieldOcc rdr PlaceHolder
-
-
--- | Represents an *occurrence* of a field that is potentially
--- ambiguous after the renamer, with the ambiguity resolved by the
--- typechecker.  We always store the 'RdrName' that the user
--- originally wrote, and store the selector function after the renamer
--- (for unambiguous occurrences) or the typechecker (for ambiguous
--- occurrences).
---
--- See Note [HsRecField and HsRecUpdField] in HsPat and
--- Note [Disambiguating record fields] in TcExpr.
--- See Note [Located RdrNames] in HsExpr
-data AmbiguousFieldOcc name
-  = Unambiguous (Located RdrName) (PostRn name name)
-  | Ambiguous   (Located RdrName) (PostTc name name)
-  deriving (Typeable)
-deriving instance ( Data name
-                  , Data (PostRn name name)
-                  , Data (PostTc name name))
-                  => Data (AmbiguousFieldOcc name)
-
-instance Outputable (AmbiguousFieldOcc name) where
-  ppr = ppr . rdrNameAmbiguousFieldOcc
-
-instance OutputableBndr (AmbiguousFieldOcc name) where
-  pprInfixOcc  = pprInfixOcc . rdrNameAmbiguousFieldOcc
-  pprPrefixOcc = pprPrefixOcc . rdrNameAmbiguousFieldOcc
-
-mkAmbiguousFieldOcc :: Located RdrName -> AmbiguousFieldOcc RdrName
-mkAmbiguousFieldOcc rdr = Unambiguous rdr PlaceHolder
-
-rdrNameAmbiguousFieldOcc :: AmbiguousFieldOcc name -> RdrName
-rdrNameAmbiguousFieldOcc (Unambiguous (L _ rdr) _) = rdr
-rdrNameAmbiguousFieldOcc (Ambiguous   (L _ rdr) _) = rdr
-
-selectorAmbiguousFieldOcc :: AmbiguousFieldOcc Id -> Id
-selectorAmbiguousFieldOcc (Unambiguous _ sel) = sel
-selectorAmbiguousFieldOcc (Ambiguous   _ sel) = sel
-
-unambiguousFieldOcc :: AmbiguousFieldOcc Id -> FieldOcc Id
-unambiguousFieldOcc (Unambiguous rdr sel) = FieldOcc rdr sel
-unambiguousFieldOcc (Ambiguous   rdr sel) = FieldOcc rdr sel
-
-ambiguousFieldOcc :: FieldOcc name -> AmbiguousFieldOcc name
-ambiguousFieldOcc (FieldOcc rdr sel) = Unambiguous rdr sel
-
 -- Takes details and result type of a GADT data constructor as created by the
 -- parser and rejigs them using information about fixities from the renamer.
 -- See Note [Sorting out the result type] in RdrHsSyn
@@ -925,9 +858,6 @@ hsLTyVarBndrsToTypes :: LHsQTyVars name -> [LHsType name]
 hsLTyVarBndrsToTypes (HsQTvs { hsq_explicit = tvbs }) = map hsLTyVarBndrToType tvbs
 
 ---------------------
-mkAnonWildCardTy :: HsType RdrName
-mkAnonWildCardTy = HsWildCardTy (AnonWildCard PlaceHolder)
-
 wildCardName :: HsWildCardInfo Name -> Name
 wildCardName (AnonWildCard  (L _ n)) = n
 
@@ -936,12 +866,118 @@ sameWildCard :: Located (HsWildCardInfo name)
              -> Located (HsWildCardInfo name) -> Bool
 sameWildCard (L l1 (AnonWildCard _))   (L l2 (AnonWildCard _))   = l1 == l2
 
+ignoreParens :: LHsType name -> LHsType name
+ignoreParens (L _ (HsParTy ty))                      = ignoreParens ty
+ignoreParens (L _ (HsAppsTy [L _ (HsAppPrefix ty)])) = ignoreParens ty
+ignoreParens ty                                      = ty
+
+{-
+************************************************************************
+*                                                                      *
+                Building types
+*                                                                      *
+************************************************************************
+-}
+
+mkAnonWildCardTy :: HsType RdrName
+mkAnonWildCardTy = HsWildCardTy (AnonWildCard PlaceHolder)
+
+mkHsOpTy :: LHsType name -> Located name -> LHsType name -> HsType name
+mkHsOpTy ty1 op ty2 = HsOpTy ty1 op ty2
+
+mkHsAppTy :: LHsType name -> LHsType name -> LHsType name
+mkHsAppTy t1 t2 = addCLoc t1 t2 (HsAppTy t1 t2)
+
+mkHsAppTys :: LHsType name -> [LHsType name] -> LHsType name
+mkHsAppTys = foldl mkHsAppTy
+
+
+{-
+************************************************************************
+*                                                                      *
+                Decomposing HsTypes
+*                                                                      *
+************************************************************************
+-}
+
+---------------------------------
+-- splitHsFunType decomposes a type (t1 -> t2 ... -> tn)
+-- Breaks up any parens in the result type:
+--      splitHsFunType (a -> (b -> c)) = ([a,b], c)
+-- Also deals with (->) t1 t2; that is why it only works on LHsType Name
+--   (see Trac #9096)
+splitHsFunType :: LHsType Name -> ([LHsType Name], LHsType Name)
+splitHsFunType (L _ (HsParTy ty))
+  = splitHsFunType ty
+
+splitHsFunType (L _ (HsFunTy x y))
+  | (args, res) <- splitHsFunType y
+  = (x:args, res)
+
+splitHsFunType orig_ty@(L _ (HsAppTy t1 t2))
+  = go t1 [t2]
+  where  -- Look for (->) t1 t2, possibly with parenthesisation
+    go (L _ (HsTyVar (L _ fn))) tys | fn == funTyConName
+                                 , [t1,t2] <- tys
+                                 , (args, res) <- splitHsFunType t2
+                                 = (t1:args, res)
+    go (L _ (HsAppTy t1 t2)) tys = go t1 (t2:tys)
+    go (L _ (HsParTy ty))    tys = go ty tys
+    go _                     _   = ([], orig_ty)  -- Failure to match
+
+splitHsFunType other = ([], other)
+
+--------------------------------
+-- | Retrieves the head of an HsAppsTy, if this can be done unambiguously,
+-- without consulting fixities.
+getAppsTyHead_maybe :: [LHsAppType name] -> Maybe (LHsType name, [LHsType name])
+getAppsTyHead_maybe tys = case splitHsAppsTy tys of
+  ([app1:apps], []) ->  -- no symbols, some normal types
+    Just (mkHsAppTys app1 apps, [])
+  ([app1l:appsl, app1r:appsr], [L loc op]) ->  -- one operator
+    Just (L loc (HsTyVar (L loc op)), [mkHsAppTys app1l appsl, mkHsAppTys app1r appsr])
+  _ -> -- can't figure it out
+    Nothing
+
+-- | Splits a [HsAppType name] (the payload of an HsAppsTy) into regions of prefix
+-- types (normal types) and infix operators.
+-- If @splitHsAppsTy tys = (non_syms, syms)@, then @tys@ starts with the first
+-- element of @non_syms@ followed by the first element of @syms@ followed by
+-- the next element of @non_syms@, etc. It is guaranteed that the non_syms list
+-- has one more element than the syms list.
+splitHsAppsTy :: [LHsAppType name] -> ([[LHsType name]], [Located name])
+splitHsAppsTy = go [] [] []
+  where
+    go acc acc_non acc_sym [] = (reverse (reverse acc : acc_non), reverse acc_sym)
+    go acc acc_non acc_sym (L _ (HsAppPrefix ty) : rest)
+      = go (ty : acc) acc_non acc_sym rest
+    go acc acc_non acc_sym (L _ (HsAppInfix op) : rest)
+      = go [] (reverse acc : acc_non) (op : acc_sym) rest
+
+-- Retrieve the name of the "head" of a nested type application
+-- somewhat like splitHsAppTys, but a little more thorough
+-- used to examine the result of a GADT-like datacon, so it doesn't handle
+-- *all* cases (like lists, tuples, (~), etc.)
+hsTyGetAppHead_maybe :: LHsType name -> Maybe (Located name, [LHsType name])
+hsTyGetAppHead_maybe = go []
+  where
+    go tys (L _ (HsTyVar ln))           = Just (ln, tys)
+    go tys (L _ (HsAppsTy apps))
+      | Just (head, args) <- getAppsTyHead_maybe apps
+                                         = go (args ++ tys) head
+    go tys (L _ (HsAppTy l r))           = go (r : tys) l
+    go tys (L _ (HsOpTy l (L loc n) r))  = Just (L loc n, l : r : tys)
+    go tys (L _ (HsParTy t))             = go tys t
+    go tys (L _ (HsKindSig t _))         = go tys t
+    go _   _                             = Nothing
+
 splitHsAppTys :: LHsType Name -> [LHsType Name] -> (LHsType Name, [LHsType Name])
   -- no need to worry about HsAppsTy here
 splitHsAppTys (L _ (HsAppTy f a)) as = splitHsAppTys f (a:as)
 splitHsAppTys (L _ (HsParTy f))   as = splitHsAppTys f as
 splitHsAppTys f                   as = (f,as)
 
+--------------------------------
 splitLHsPatSynTy :: LHsType name
                  -> ( [LHsTyVarBndr name]
                     , LHsContext name        -- Required
@@ -974,48 +1010,101 @@ splitLHsQualTy :: LHsType name -> (LHsContext name, LHsType name)
 splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt,     body)
 splitLHsQualTy body                                                  = (noLoc [], body)
 
-splitLHsInstDeclTy
-    :: LHsSigType Name
-    -> ([Name], LHsContext Name, LHsType Name)
-        -- Split up an instance decl type, returning the pieces
+splitLHsInstDeclTy :: LHsSigType Name
+                   -> ([Name], LHsContext Name, LHsType Name)
+-- Split up an instance decl type, returning the pieces
 splitLHsInstDeclTy (HsIB { hsib_vars = itkvs
                          , hsib_body = inst_ty })
-  = (itkvs, cxt, body_ty)
+  | (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty
+  = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
          -- Return implicitly bound type and kind vars
          -- For an instance decl, all of them are in scope
   where
-    (cxt, body_ty) = splitLHsQualTy inst_ty
 
--- splitHsFunType decomposes a type (t1 -> t2 ... -> tn)
--- Breaks up any parens in the result type:
---      splitHsFunType (a -> (b -> c)) = ([a,b], c)
--- Also deals with (->) t1 t2; that is why it only works on LHsType Name
---   (see Trac #9096)
-splitHsFunType :: LHsType Name -> ([LHsType Name], LHsType Name)
-splitHsFunType (L _ (HsParTy ty))
-  = splitHsFunType ty
+getLHsInstDeclHead :: LHsSigType name -> LHsType name
+getLHsInstDeclHead inst_ty
+  | (_tvs, _cxt, body_ty) <- splitLHsSigmaTy (hsSigType inst_ty)
+  = body_ty
 
-splitHsFunType (L _ (HsFunTy x y))
-  | (args, res) <- splitHsFunType y
-  = (x:args, res)
+getLHsInstDeclClass_maybe :: LHsSigType name -> Maybe (Located name)
+-- Works on (HsSigType RdrName)
+getLHsInstDeclClass_maybe inst_ty
+  = do { let head_ty = getLHsInstDeclHead inst_ty
+       ; (cls, _) <- hsTyGetAppHead_maybe head_ty
+       ; return cls }
 
-splitHsFunType orig_ty@(L _ (HsAppTy t1 t2))
-  = go t1 [t2]
-  where  -- Look for (->) t1 t2, possibly with parenthesisation
-    go (L _ (HsTyVar (L _ fn))) tys | fn == funTyConName
-                                 , [t1,t2] <- tys
-                                 , (args, res) <- splitHsFunType t2
-                                 = (t1:args, res)
-    go (L _ (HsAppTy t1 t2)) tys = go t1 (t2:tys)
-    go (L _ (HsParTy ty))    tys = go ty tys
-    go _                     _   = ([], orig_ty)  -- Failure to match
+{-
+************************************************************************
+*                                                                      *
+                FieldOcc
+*                                                                      *
+************************************************************************
+-}
 
-splitHsFunType other = ([], other)
+type LFieldOcc name = Located (FieldOcc name)
 
-ignoreParens :: LHsType name -> LHsType name
-ignoreParens (L _ (HsParTy ty))                      = ignoreParens ty
-ignoreParens (L _ (HsAppsTy [L _ (HsAppPrefix ty)])) = ignoreParens ty
-ignoreParens ty                                      = ty
+-- | Represents an *occurrence* of an unambiguous field.  We store
+-- both the 'RdrName' the user originally wrote, and after the
+-- renamer, the selector function.
+data FieldOcc name = FieldOcc { rdrNameFieldOcc  :: Located RdrName
+                                 -- ^ See Note [Located RdrNames] in HsExpr
+                              , selectorFieldOcc :: PostRn name name
+                              }
+  deriving Typeable
+deriving instance Eq (PostRn name name) => Eq (FieldOcc name)
+deriving instance Ord (PostRn name name) => Ord (FieldOcc name)
+deriving instance (Data name, Data (PostRn name name)) => Data (FieldOcc name)
+
+instance Outputable (FieldOcc name) where
+  ppr = ppr . rdrNameFieldOcc
+
+mkFieldOcc :: Located RdrName -> FieldOcc RdrName
+mkFieldOcc rdr = FieldOcc rdr PlaceHolder
+
+
+-- | Represents an *occurrence* of a field that is potentially
+-- ambiguous after the renamer, with the ambiguity resolved by the
+-- typechecker.  We always store the 'RdrName' that the user
+-- originally wrote, and store the selector function after the renamer
+-- (for unambiguous occurrences) or the typechecker (for ambiguous
+-- occurrences).
+--
+-- See Note [HsRecField and HsRecUpdField] in HsPat and
+-- Note [Disambiguating record fields] in TcExpr.
+-- See Note [Located RdrNames] in HsExpr
+data AmbiguousFieldOcc name
+  = Unambiguous (Located RdrName) (PostRn name name)
+  | Ambiguous   (Located RdrName) (PostTc name name)
+  deriving (Typeable)
+deriving instance ( Data name
+                  , Data (PostRn name name)
+                  , Data (PostTc name name))
+                  => Data (AmbiguousFieldOcc name)
+
+instance Outputable (AmbiguousFieldOcc name) where
+  ppr = ppr . rdrNameAmbiguousFieldOcc
+
+instance OutputableBndr (AmbiguousFieldOcc name) where
+  pprInfixOcc  = pprInfixOcc . rdrNameAmbiguousFieldOcc
+  pprPrefixOcc = pprPrefixOcc . rdrNameAmbiguousFieldOcc
+
+mkAmbiguousFieldOcc :: Located RdrName -> AmbiguousFieldOcc RdrName
+mkAmbiguousFieldOcc rdr = Unambiguous rdr PlaceHolder
+
+rdrNameAmbiguousFieldOcc :: AmbiguousFieldOcc name -> RdrName
+rdrNameAmbiguousFieldOcc (Unambiguous (L _ rdr) _) = rdr
+rdrNameAmbiguousFieldOcc (Ambiguous   (L _ rdr) _) = rdr
+
+selectorAmbiguousFieldOcc :: AmbiguousFieldOcc Id -> Id
+selectorAmbiguousFieldOcc (Unambiguous _ sel) = sel
+selectorAmbiguousFieldOcc (Ambiguous   _ sel) = sel
+
+unambiguousFieldOcc :: AmbiguousFieldOcc Id -> FieldOcc Id
+unambiguousFieldOcc (Unambiguous rdr sel) = FieldOcc rdr sel
+unambiguousFieldOcc (Ambiguous   rdr sel) = FieldOcc rdr sel
+
+ambiguousFieldOcc :: FieldOcc name -> AmbiguousFieldOcc name
+ambiguousFieldOcc (FieldOcc rdr sel) = Unambiguous rdr sel
 
 {-
 ************************************************************************
index abd7a4b..cb2da5c 100644 (file)
@@ -56,8 +56,6 @@ module HsUtils(
   mkHsAppTy, mkHsAppTys, userHsTyVarBndrs, userHsLTyVarBndrs,
   mkLHsSigType, mkLHsSigWcType, mkClassOpSigs,
   nlHsAppTy, nlHsTyVar, nlHsFunTy, nlHsTyConApp,
-  getAppsTyHead_maybe, hsTyGetAppHead_maybe, splitHsAppsTy,
-  getLHsInstDeclClass_maybe,
 
   -- Stmts
   mkTransformStmt, mkTransformByStmt, mkBodyStmt, mkBindStmt, mkTcBindStmt,
@@ -168,12 +166,6 @@ mkMatchGroupName origin matches = MG { mg_alts = mkLocatedList matches
                                      , mg_res_ty = placeHolderType
                                      , mg_origin = origin }
 
-mkHsAppTy :: LHsType name -> LHsType name -> LHsType name
-mkHsAppTy t1 t2 = addCLoc t1 t2 (HsAppTy t1 t2)
-
-mkHsAppTys :: LHsType name -> [LHsType name] -> LHsType name
-mkHsAppTys = foldl mkHsAppTy
-
 mkHsApp :: LHsExpr name -> LHsExpr name -> LHsExpr name
 mkHsApp e1 e2 = addCLoc e1 e2 (HsApp e1 e2)
 
@@ -1141,60 +1133,3 @@ lPatImplicits = hs_lpat
                                                           pat_explicit = maybe True (i<) (rec_dotdot fs)]
     details (InfixCon p1 p2) = hs_lpat p1 `unionNameSet` hs_lpat p2
 
-{-
-************************************************************************
-*                                                                      *
-   Dealing with HsAppsTy
-*                                                                      *
-************************************************************************
--}
-
--- | Retrieves the head of an HsAppsTy, if this can be done unambiguously,
--- without consulting fixities.
-getAppsTyHead_maybe :: [LHsAppType name] -> Maybe (LHsType name, [LHsType name])
-getAppsTyHead_maybe tys = case splitHsAppsTy tys of
-  ([app1:apps], []) ->  -- no symbols, some normal types
-    Just (mkHsAppTys app1 apps, [])
-  ([app1l:appsl, app1r:appsr], [L loc op]) ->  -- one operator
-    Just (L loc (HsTyVar (L loc op)), [mkHsAppTys app1l appsl, mkHsAppTys app1r appsr])
-  _ -> -- can't figure it out
-    Nothing
-
--- | Splits a [HsAppType name] (the payload of an HsAppsTy) into regions of prefix
--- types (normal types) and infix operators.
--- If @splitHsAppsTy tys = (non_syms, syms)@, then @tys@ starts with the first
--- element of @non_syms@ followed by the first element of @syms@ followed by
--- the next element of @non_syms@, etc. It is guaranteed that the non_syms list
--- has one more element than the syms list.
-splitHsAppsTy :: [LHsAppType name] -> ([[LHsType name]], [Located name])
-splitHsAppsTy = go [] [] []
-  where
-    go acc acc_non acc_sym [] = (reverse (reverse acc : acc_non), reverse acc_sym)
-    go acc acc_non acc_sym (L _ (HsAppPrefix ty) : rest)
-      = go (ty : acc) acc_non acc_sym rest
-    go acc acc_non acc_sym (L _ (HsAppInfix op) : rest)
-      = go [] (reverse acc : acc_non) (op : acc_sym) rest
-
--- retrieve the name of the "head" of a nested type application
--- somewhat like splitHsAppTys, but a little more thorough
--- used to examine the result of a GADT-like datacon, so it doesn't handle
--- *all* cases (like lists, tuples, (~), etc.)
-hsTyGetAppHead_maybe :: LHsType name -> Maybe (Located name, [LHsType name])
-hsTyGetAppHead_maybe = go []
-  where
-    go tys (L _ (HsTyVar ln))           = Just (ln, tys)
-    go tys (L _ (HsAppsTy apps))
-      | Just (head, args) <- getAppsTyHead_maybe apps
-                                         = go (args ++ tys) head
-    go tys (L _ (HsAppTy l r))           = go (r : tys) l
-    go tys (L _ (HsOpTy l (L loc n) r))  = Just (L loc n, l : r : tys)
-    go tys (L _ (HsParTy t))             = go tys t
-    go tys (L _ (HsKindSig t _))         = go tys t
-    go _   _                             = Nothing
-
-getLHsInstDeclClass_maybe :: LHsSigType name -> Maybe (Located name)
--- Works on (HsSigType RdrName)
-getLHsInstDeclClass_maybe inst_ty
-  = do { let (_, tau) = splitLHsQualTy (hsSigType inst_ty)
-       ; (cls, _) <- hsTyGetAppHead_maybe tau
-       ; return cls }
index 98aacd0..4f65509 100644 (file)
@@ -633,8 +633,7 @@ checkCanonicalInstances cls poly_ty mbinds = do
     -- stolen from TcInstDcls
     instDeclCtxt1 :: LHsSigType Name -> SDoc
     instDeclCtxt1 hs_inst_ty
-      | (_, _, head_ty) <- splitLHsInstDeclTy hs_inst_ty
-      = inst_decl_ctxt (ppr head_ty)
+      = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
 
     inst_decl_ctxt :: SDoc -> SDoc
     inst_decl_ctxt doc = hang (text "in the instance declaration for")
index 2d5372d..292187b 100644 (file)
@@ -833,7 +833,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
   = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
                         -- Include kind variables!  Trac #7916
              my_theta = pickQuantifiablePreds free_tvs inferred_theta
-             binders  = [ mkNamedBinder tv Invisible
+             binders  = [ mkNamedBinder Invisible tv
                         | tv <- qtvs
                         , tv `elemVarSet` free_tvs ]
        ; return (binders, my_theta) }
@@ -892,7 +892,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
 
     spec_tv_set = mkVarSet $ map snd annotated_tvs
     mk_binders free_tvs
-      = [ mkNamedBinder tv vis
+      = [ mkNamedBinder vis tv
         | tv <- qtvs
         , tv `elemVarSet` free_tvs
         , let vis | tv `elemVarSet` spec_tv_set = Specified
index e438df5..f5537b6 100644 (file)
@@ -232,28 +232,13 @@ tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
                 -> LHsSigType Name
                 -> TcM ([TyVar], ThetaType, Class, [Type])
 -- Like tcHsSigType, but for a class instance declaration
--- The significant difference is that we expect a /constraint/
--- not a /type/ for the bit after the '=>'.
-tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars
-                                           , hsib_body = hs_qual_ty })
-    -- An explicit forall in an instance declaration isn't
-    -- allowed, so there won't be any HsForAllTy here
-  = setSrcSpan (getLoc hs_qual_ty) $
-    do { (tkvs, phi_ty) <- solveEqualities $
-                           tcImplicitTKBndrsType sig_vars $
-                    do { theta    <- tcHsContext cxt
-                       ; head_ty' <- tc_lhs_type typeLevelMode
-                                                 head_ty constraintKind
-                       ; return (mkPhiTy theta head_ty') }
-       ; let inst_ty = mkSpecForAllTys tkvs phi_ty
+tcHsClsInstType user_ctxt hs_inst_ty
+  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
+    do { inst_ty <- tc_hs_sig_type hs_inst_ty constraintKind
        ; inst_ty <- kindGeneralizeType inst_ty
-       ; inst_ty <- zonkTcType inst_ty
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
-  where
-    (cxt, head_ty) = splitLHsQualTy hs_qual_ty
 
 -- Used for 'VECTORISE [SCALAR] instance' declarations
---
 tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type])
 tcHsVectInst ty
   | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
@@ -478,7 +463,7 @@ tc_fun_type mode ty1 ty2 exp_kind
        ; res_lev <- newFlexiTyVarTy levityTy
        ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev)
        ; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev)
-       ; checkExpectedKind (mkNakedFunTy ty1' ty2') liftedTypeKind exp_kind }
+       ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
 
 ------------------------------------------
 -- See also Note [Bidirectional type checking]
@@ -508,34 +493,32 @@ tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
   = tc_fun_type mode ty1 ty2 exp_kind
 
 --------- Foralls
-tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
-    -- Do not kind-generalise here.  See Note [Kind generalisation]
-  | isConstraintKind exp_kind
-  = failWithTc (hang (text "Illegal constraint:") 2 (ppr hs_ty))
-
-  | otherwise
+tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
   = fmap fst $
     tcExplicitTKBndrs hs_tvs $ \ tvs' ->
     -- Do not kind-generalise here!  See Note [Kind generalisation]
-    -- Why exp_kind?  See Note [Body kind of forall]
+    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
     do { ty' <- tc_lhs_type mode ty exp_kind
        ; let bound_vars = allBoundVariables ty'
-       ; return (mkNakedSpecSigmaTy tvs' [] ty', bound_vars) }
+             bndrs      = map (mkNamedBinder Specified) tvs'
+       ; return (mkForAllTys bndrs ty', bound_vars) }
 
 tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
+  | null (unLoc ctxt)
+  = tc_lhs_type mode ty exp_kind
+
+  | otherwise
   = do { ctxt' <- tc_hs_context mode ctxt
-       ; ty' <- if null (unLoc ctxt) then  -- Plain forall, no context
-                   tc_lhs_type mode ty exp_kind
-                     -- Why exp_kind?  See Note [Body kind of forall]
-                else
-                   -- If there is a context, then this forall is really a
-                   -- _function_, so the kind of the result really is *
-                   -- The body kind (result of the function) can be * or #, hence ekOpen
-                   do { ek <- ekOpen
-                      ; ty <- tc_lhs_type mode ty ek
-                      ; checkExpectedKind ty liftedTypeKind exp_kind }
-
-       ; return (mkNakedPhiTy ctxt' ty') }
+
+         -- See Note [Body kind of a HsQualTy]
+       ; ty' <- if isConstraintKind exp_kind
+                then tc_lhs_type mode ty constraintKind
+                else do { ek <- ekOpen -- The body kind (result of the
+                                       -- function) can be * or #, hence ekOpen
+                        ; ty <- tc_lhs_type mode ty ek
+                        ; checkExpectedKind ty liftedTypeKind exp_kind }
+
+       ; return (mkPhiTy ctxt' ty') }
 
 --------- Lists, arrays, and tuples
 tc_hs_type mode (HsListTy elt_ty) exp_kind
@@ -1101,8 +1084,8 @@ look at the TyCon or Class involved.
 This is horribly delicate.  I hate it.  A good example of how
 delicate it is can be seen in Trac #7903.
 
-Note [Body kind of a forall]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Body kind of a HsForAllTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The body of a forall is usually a type, but in principle
 there's no reason to prohibit *unlifted* types.
 In fact, GHC can itself construct a function with an
@@ -1112,37 +1095,6 @@ typecheck/should_compile/tc170).
 Moreover in instance heads we get forall-types with
 kind Constraint.
 
-Moreover if we have a signature
-   f :: Int#
-then we represent it as (HsForAll Implicit [] [] Int#).  And this must
-be legal!  We can't drop the empty forall until *after* typechecking
-the body because of kind polymorphism:
-   Typeable :: forall k. k -> Constraint
-   data Apply f t = Apply (f t)
-   -- Apply :: forall k. (k -> *) -> k -> *
-   instance Typeable Apply where ...
-Then the dfun has type
-   df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)
-
-   f :: Typeable Apply
-
-   f :: forall (t:k->*) (a:k).  t a -> t a
-
-   class C a b where
-      op :: a b -> Typeable Apply
-
-   data T a = MkT (Typeable Apply)
-            | T2 a
-      T :: * -> *
-      MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a
-
-   f :: (forall (k:*). forall (t:: k->*) (a:k). t a -> t a) -> Int
-   f :: (forall a. a -> Typeable Apply) -> Int
-
-So we *must* keep the HsForAll on the instance type
-   HsForAll Implicit [] [] (Typeable Apply)
-so that we do kind generalisation on it.
-
 It's tempting to check that the body kind is either * or #. But this is
 wrong. For example:
 
@@ -1154,6 +1106,33 @@ the predicate `C a`. So we quantify, yielding `forall a. C a` even though
 `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
 convenient. Bottom line: don't check for * or # here.
 
+Note [Body kind of a HsQualTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If ctxt is non-empty, the HsQualTy really is a /function/, so the
+kind of the result really is '*', and in that case the kind of the
+body-type can be lifted or unlifted.
+
+However, consider
+    instance Eq a => Eq [a] where ...
+or
+    f :: (Eq a => Eq [a]) => blah
+Here both body-kind of the HsQualTy is Constraint rather than *.
+Rather crudely we tell the difference by looking at exp_kind. It's
+very convenient to typecheck instance types like any other HsSigType.
+
+Admittedly the '(Eq a => Eq [a]) => blah' case is erroneous, but it's
+better to reject in checkValidType.  If we say that the body kind
+should be '*' we risk getting TWO error messages, one saying that Eq
+[a] doens't have kind '*', and one saying that we need a Constraint to
+the left of the outer (=>).
+
+How do we figure out the right body kind?  Well, it's a bit of a
+kludge: I just look at the expected kind.  If it's Constraint, we
+must be in this instance situation context. It's a kludge because it
+wouldn't work if any unification was involved to compute that result
+kind -- but it isn't.  (The true way might be to use the 'mode'
+parameter, but that seemed like a sledgehammer to crack a nut.)
+
 Note [Inferring tuple kinds]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
@@ -1338,7 +1317,7 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
            ; let k_fvs = tyCoVarsOfType k
                  (bndr, fvs')
                    | tv `elemVarSet` fvs
-                   = ( mkNamedBinder tv Visible
+                   = ( mkNamedBinder Visible tv
                      , fvs `delVarSet` tv `unionVarSet` k_fvs )
                    | otherwise
                    = (mkAnonBinder k, fvs `unionVarSet` k_fvs)
@@ -1490,6 +1469,7 @@ new_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv
 
 ------------------
 kindGeneralizeType :: Type -> TcM Type
+-- Result is zonked
 kindGeneralizeType ty
   = do { kvs <- kindGeneralize ty
        ; zonkTcType (mkInvForAllTys kvs ty) }
index 48a8b99..9a0360e 100644 (file)
@@ -1755,8 +1755,7 @@ tcSpecInst _  _ = panic "tcSpecInst"
 
 instDeclCtxt1 :: LHsSigType Name -> SDoc
 instDeclCtxt1 hs_inst_ty
-  | (_, _, head_ty) <- splitLHsInstDeclTy hs_inst_ty
-  = inst_decl_ctxt (ppr head_ty)
+  = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
 
 instDeclCtxt2 :: Type -> SDoc
 instDeclCtxt2 dfun_ty
index 63c06af..0640b91 100644 (file)
@@ -50,8 +50,8 @@ module TcType (
   --------------------------------
   -- Builders
   mkPhiTy, mkInvSigmaTy, mkSpecSigmaTy, mkSigmaTy,
-  mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy, mkNakedFunTy,
-  mkNakedSpecSigmaTy, mkNakedCastTy, mkNakedPhiTy,
+  mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
+  mkNakedCastTy,
 
   --------------------------------
   -- Splitters
@@ -989,30 +989,17 @@ mkSigmaTy bndrs theta tau = mkForAllTys bndrs (mkPhiTy theta tau)
 
 mkInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 mkInvSigmaTy tyvars
-  = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Invisible))
+  = mkSigmaTy (map (mkNamedBinder Invisible) tyvars)
 
 -- | Make a sigma ty where all type variables are "specified". That is,
 -- they can be used with visible type application
 mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 mkSpecSigmaTy tyvars
-  = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified))
+  = mkSigmaTy (map (mkNamedBinder Specified) tyvars)
 
 mkPhiTy :: [PredType] -> Type -> Type
 mkPhiTy = mkFunTys
 
-mkNakedSigmaTy :: [TyBinder] -> [PredType] -> Type -> Type
--- See Note [Type-checking inside the knot] in TcHsType
-mkNakedSigmaTy bndrs theta tau = mkForAllTys bndrs (mkNakedPhiTy theta tau)
-
-mkNakedSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
--- See Note [Type-checking inside the knot] in TcHsType
-mkNakedSpecSigmaTy tyvars
-  = mkNakedSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified))
-
-mkNakedPhiTy :: [PredType] -> Type -> Type
--- See Note [Type-checking inside the knot] in TcHsType
-mkNakedPhiTy = flip $ foldr mkNakedFunTy
-
 -- @isTauTy@ tests if a type is "simple"..
 isTauTy :: Type -> Bool
 isTauTy ty | Just ty' <- coreView ty = isTauTy ty'
@@ -1067,10 +1054,6 @@ mkNakedAppTy :: Type -> Type -> Type
 -- See Note [Type-checking inside the knot] in TcHsType
 mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
 
-mkNakedFunTy :: Type -> Type -> Type
--- See Note [Type-checking inside the knot] in TcHsType
-mkNakedFunTy arg res = ForAllTy (Anon arg) res
-
 mkNakedCastTy :: Type -> Coercion -> Type
 mkNakedCastTy = CastTy
 
index 31e53f0..56cb348 100644 (file)
@@ -412,10 +412,12 @@ data Rank = ArbitraryRank         -- Any rank ok
 
           | MustBeMonoType  -- Monotype regardless of flags
 
-rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
-rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
-tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
-synArgMonoType   = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
+
+rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
+rankZeroMonoType   = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
+tyConArgMonoType   = MonoType (text "GHC doesn't yet support impredicative polymorphism")
+synArgMonoType     = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
+constraintMonoType = MonoType (text "A constraint must be a monotype")
 
 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result
 funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
@@ -454,7 +456,8 @@ check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
 
 check_type env ctxt rank ty
   | not (null tvs && null theta)
-  = do  { checkTcM (forAllAllowed rank) (forAllTyErr env' rank ty)
+  = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
+        ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
 
@@ -594,9 +597,12 @@ check_arg_type env ctxt rank ty
 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
 forAllTyErr env rank ty
    = ( env
-     , vcat [ hang (text "Illegal polymorphic or qualified type:") 2 (ppr_tidy env ty)
+     , vcat [ hang herald 2 (ppr_tidy env ty)
             , suggestion ] )
   where
+    (tvs, _theta, _tau) = tcSplitSigmaTy ty
+    herald | null tvs  = text "Illegal qualified type:"
+           | otherwise = text "Illegal polymorphic type:"
     suggestion = case rank of
                    LimitedRank {} -> text "Perhaps you intended to use RankNTypes or Rank2Types"
                    MonoType d     -> d
@@ -714,7 +720,7 @@ check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
 -- Check the validity of a predicate in a signature
 -- See Note [Validity checking for constraints]
 check_pred_ty env dflags ctxt pred
-  = do { check_type env SigmaCtxt MustBeMonoType pred
+  = do { check_type env SigmaCtxt constraintMonoType pred
        ; check_pred_help False env dflags ctxt pred }
 
 check_pred_help :: Bool    -- True <=> under a type synonym
@@ -1183,8 +1189,7 @@ checkValidInstance ctxt hs_type ty
     (tvs, theta, tau) = tcSplitSigmaTy ty
 
         -- The location of the "head" of the instance
-    head_loc = case splitLHsInstDeclTy hs_type of
-                 (_, _, L loc _) -> loc
+    head_loc = getLoc (getLHsInstDeclHead hs_type)
 
 {-
 Note [Paterson conditions]
index 5b2fb4f..c8e48c0 100644 (file)
@@ -307,7 +307,7 @@ ppr_co_ax_branch ppr_rhs
                           , cab_rhs = rhs
                           , cab_loc = loc })
   = foldr1 (flip hangNotEmpty 2)
-        [ pprUserForAll (map (flip mkNamedBinder Invisible) (tvs ++ cvs))
+        [ pprUserForAll (map (mkNamedBinder Invisible) (tvs ++ cvs))
         , pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
         , text "-- Defined" <+> pprLoc loc ]
   where
index 3576fdd..b4345ed 100644 (file)
@@ -454,8 +454,7 @@ mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
 infixr 3 `mkFunTy`      -- Associates to the right
 -- | Make an arrow type
 mkFunTy :: Type -> Type -> Type
-mkFunTy arg res
-  = ForAllTy (Anon arg) res
+mkFunTy arg res = ForAllTy (Anon arg) res
 
 -- | Make nested arrow types
 mkFunTys :: [Type] -> Type -> Type
index 12befed..67365e3 100644 (file)
@@ -1406,13 +1406,17 @@ applyTys :: Type -> [KindOrType] -> Type
 applyTys ty args = applyTysD empty ty args
 
 applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
-applyTysD _   orig_fun_ty []      = orig_fun_ty
 applyTysD doc orig_fun_ty arg_tys
+  | null arg_tys
+  = orig_fun_ty
+
   | n_bndrs == n_args     -- The vastly common case
   = substTyWithBindersUnchecked bndrs arg_tys rho_ty
+
   | n_bndrs > n_args      -- Too many for-alls
   = substTyWithBindersUnchecked (take n_args bndrs) arg_tys
                                 (mkForAllTys (drop n_args bndrs) rho_ty)
+
   | otherwise             -- Too many type args
   = ASSERT2( n_bndrs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys )       -- Zero case gives infinite loop!
     applyTysD doc (substTyWithBinders bndrs (take n_bndrs arg_tys) rho_ty)
@@ -1440,8 +1444,8 @@ applyTysX tvs body_ty arg_tys
 -}
 
 -- | Make a named binder
-mkNamedBinder :: Var -> VisibilityFlag -> TyBinder
-mkNamedBinder = Named
+mkNamedBinder :: VisibilityFlag -> Var -> TyBinder
+mkNamedBinder vis var = Named var vis
 
 -- | Make an anonymous binder
 mkAnonBinder :: Type -> TyBinder
@@ -1510,40 +1514,56 @@ partitionBindersIntoBinders = partitionWith named_or_anon
 ************************************************************************
 
 Predicates on PredType
+
+Note [isPredTy complications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You would think that we could define
+  isPredTy ty = isConstraintKind (typeKind ty)
+But there are a number of complications:
+
+* isPredTy is used when printing types, which can happen in debug
+  printing during type checking of not-fully-zonked types.  So it's
+  not cool to say isConstraintKind (typeKind ty) because, absent
+  zonking, the type might be ill-kinded, and typeKind crashes. Hence the
+  rather tiresome story here
+
+* isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
+  and (t1 ~R# t2), which are not of kind Constraint!  Currently they are
+  of kind #.
+
+* If we do form the type '(C a => C [a]) => blah', then we'd like to
+  print it as such. But that means that isPredTy must return True for
+  (C a => C [a]).  Admittedly that type is illegal in Haskell, but we
+  want to print it nicely in error messages.
 -}
 
 -- | Is the type suitable to classify a given/wanted in the typechecker?
 isPredTy :: Type -> Bool
-  -- NB: isPredTy is used when printing types, which can happen in debug printing
-  --     during type checking of not-fully-zonked types.  So it's not cool to say
-  --     isConstraintKind (typeKind ty) because absent zonking the type might
-  --     be ill-kinded, and typeKind crashes
-  --     Hence the rather tiresome story here
-  --
-  -- NB: This must return "True" to *unlifted* coercions, which are not
-  --     of kind Constraint!
+-- See Note [isPredTy complications]
 isPredTy ty = go ty []
   where
     go :: Type -> [KindOrType] -> Bool
-    go (AppTy ty1 ty2)   args = go ty1 (ty2 : args)
-    go (TyConApp tc tys) args
+    go (AppTy ty1 ty2)   args       = go ty1 (ty2 : args)
+    go (TyVarTy tv)      args       = go_k (tyVarKind tv) args
+    go (TyConApp tc tys) args       = ASSERT( null args )  -- TyConApp invariant
+                                      go_tc tc tys
+    go (ForAllTy (Anon arg) res) []
+      | isPredTy arg                = isPredTy res   -- (Eq a => C a)
+      | otherwise                   = False          -- (Int -> Bool)
+    go (ForAllTy (Named {}) ty) []  = go ty []
+    go _ _ = False
+
+    go_tc :: TyCon -> [KindOrType] -> Bool
+    go_tc tc args
       | tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
-      , [_,_,_,_] <- all_args
-      = True
-
-      | otherwise
-      = go_k (tyConKind tc) all_args
-      where
-        all_args = tys ++ args
-    go (TyVarTy tv)      args = go_k (tyVarKind tv) args
-    go _                 _    = False
+                  = length args == 4  -- ~# and ~R# sadly have result kind #
+                                      -- not Contraint; but we still want
+                                      -- isPredTy to reply True.
+      | otherwise = go_k (tyConKind tc) args
 
     go_k :: Kind -> [KindOrType] -> Bool
-    -- True <=> kind is k1 -> .. -> kn -> Constraint
-    go_k k [] = isConstraintKind k
-    go_k (ForAllTy bndr k1) (arg:args)
-      = go_k (substTyWithBindersUnchecked [bndr] [arg] k1) args
-    go_k _ _ = False                  -- Typeable * Int :: Constraint
+    -- True <=> ('k' applied to 'kts') = Constraint
+    go_k k args = isConstraintKind (applyTys k args)
 
 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
index c6b6a97..f298192 100644 (file)
@@ -1,5 +1,5 @@
-
-T3163.hs:8:5: error:
-    Illegal polymorphic or qualified type: forall s1. s1
-    In the definition of data constructor ‘Unreached’
-    In the data type declaration for ‘Taker’
+\r
+T3163.hs:8:5: error:\r
+    • Illegal polymorphic type: forall s. s\r
+    • In the definition of data constructor ‘Unreached’\r
+      In the data type declaration for ‘Taker’\r
index 9a10408..602fc3d 100644 (file)
@@ -1,5 +1,6 @@
 \r
 SimpleFail15.hs:5:8: error:\r
-    Illegal polymorphic or qualified type: (a ~ b) => t\r
-    Perhaps you intended to use RankNTypes or Rank2Types\r
-    In the type signature: foo :: (a, b) -> (a ~ b => t) -> (a, b)\r
+    • Illegal qualified type: (a ~ b) => t\r
+      Perhaps you intended to use RankNTypes or Rank2Types\r
+    • In the type signature:\r
+        foo :: (a, b) -> (a ~ b => t) -> (a, b)\r
index ed21c65..ae15f82 100644 (file)
@@ -1,4 +1,4 @@
-
-T10899.hs:7:3: error:
-    Illegal polymorphic or qualified type: forall (m1 :: * -> *). m1 a
-    In the class declaration for ‘C’
+\r
+T10899.hs:7:3: error:\r
+    • Illegal polymorphic type: forall (m :: * -> *). m a\r
+    • In the class declaration for ‘C’\r
index 32331e5..c0e08e7 100644 (file)
@@ -1,4 +1,4 @@
-
-T9357.hs:12:15: error:
-    • Illegal polymorphic or qualified type: forall a1. a1 -> a1
-    • In the type instance declaration for ‘F’
+\r
+T9357.hs:12:15: error:\r
+    • Illegal polymorphic type: forall a. a -> a\r
+    • In the type instance declaration for ‘F’\r
index bc717ec..cb3bae5 100644 (file)
@@ -1,14 +1,14 @@
-
-rnfail026.hs:16:10: error:
-    • Illegal polymorphic or qualified type: forall a1. Eq a1 => Set a1
-    • In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
-
-rnfail026.hs:16:27: error:
-    • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
-    • In the first argument of ‘Monad’, namely
-        ‘forall a. Eq a => Set a’
-      In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
-
-rnfail026.hs:19:10: error:
-    • Illegal polymorphic or qualified type: forall a1. [a1]
-    • In the instance declaration for ‘Eq (forall a. [a])’
+\r
+rnfail026.hs:16:10: error:\r
+    • Illegal polymorphic type: forall a. Eq a => Set a\r
+    • In the instance declaration for ‘Monad (forall a. Eq a => Set a)’\r
+\r
+rnfail026.hs:16:27: error:\r
+    • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’\r
+    • In the first argument of ‘Monad’, namely\r
+        ‘forall a. Eq a => Set a’\r
+      In the instance declaration for ‘Monad (forall a. Eq a => Set a)’\r
+\r
+rnfail026.hs:19:10: error:\r
+    • Illegal polymorphic type: forall a. [a]\r
+    • In the instance declaration for ‘Eq (forall a. [a])’\r
index cd3cc73..e902344 100644 (file)
@@ -1,9 +1,9 @@
-
-T11355.hs:5:7: error:
-    • Illegal polymorphic or qualified type: forall (a1 :: TYPE t0). a1
-      GHC doesn't yet support impredicative polymorphism
-    • In the expression:
-        const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
-      In an equation for ‘foo’:
-          foo
-            = const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
+\r
+T11355.hs:5:7: error:\r
+    • Illegal polymorphic type: forall (a :: TYPE t0). a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the expression:\r
+        const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))\r
+      In an equation for ‘foo’:\r
+          foo\r
+            = const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))\r
index a905d95..82ff1c7 100644 (file)
@@ -1,14 +1,18 @@
 \r
 T2538.hs:6:6: error:\r
-    Illegal polymorphic or qualified type: Eq a => a -> a\r
-    Perhaps you intended to use RankNTypes or Rank2Types\r
-    In the type signature: f :: (Eq a => a -> a) -> Int\r
+    • Illegal qualified type: Eq a => a -> a\r
+      Perhaps you intended to use RankNTypes or Rank2Types\r
+    • In the type signature:\r
+        f :: (Eq a => a -> a) -> Int\r
 \r
 T2538.hs:9:6: error:\r
-    Illegal polymorphic or qualified type: Eq a => a -> a\r
-    GHC doesn't yet support impredicative polymorphism\r
-    In the type signature: g :: [Eq a => a -> a] -> Int\r
+    • Illegal qualified type: Eq a => a -> a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        g :: [Eq a => a -> a] -> Int\r
 \r
 T2538.hs:12:6: error:\r
-    Illegal polymorphic or qualified type: Eq a => a -> a\r
-    In the type signature: h :: Ix (Eq a => a -> a) => Int\r
+    • Illegal qualified type: Eq a => a -> a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        h :: Ix (Eq a => a -> a) => Int\r
index c960ba9..88e0904 100644 (file)
@@ -1,5 +1,6 @@
 \r
 T5957.hs:3:9: error:\r
-    Illegal polymorphic or qualified type: Show a => a -> String\r
-    Perhaps you intended to use RankNTypes or Rank2Types\r
-    In the type signature: flex :: Int -> Show a => a -> String\r
+    • Illegal qualified type: Show a => a -> String\r
+      Perhaps you intended to use RankNTypes or Rank2Types\r
+    • In the type signature:\r
+        flex :: Int -> Show a => a -> String\r
index 6e47926..4e3bf7c 100644 (file)
@@ -1,5 +1,5 @@
-
-T7019.hs:11:12:
-    Illegal constraint: forall a. c (Free c a)
-    In the type ‘forall a. c (Free c a)’
-    In the type declaration for ‘C’
+\r
+T7019.hs:11:1: error:\r
+    • Illegal polymorphic type: forall a. c (Free c a)\r
+      A constraint must be a monotype\r
+    • In the type synonym declaration for ‘C’\r
index f888931..0cb36d3 100644 (file)
@@ -1,4 +1,7 @@
-
-T7019a.hs:11:8:
-    Illegal constraint: forall b. Context (Associated a b)
-    In the class declaration for ‘Class’
+\r
+T7019a.hs:11:1: error:\r
+    • Illegal polymorphic type: forall b. Context (Associated a b)\r
+      A constraint must be a monotype\r
+    • In the context: forall b. Context (Associated a b)\r
+      While checking the super-classes of class ‘Class’\r
+      In the class declaration for ‘Class’\r
index aa44b44..3a85051 100644 (file)
@@ -1,5 +1,6 @@
 \r
 T7809.hs:8:8: error:\r
-    Illegal polymorphic or qualified type: PolyId\r
-    GHC doesn't yet support impredicative polymorphism\r
-    In the type signature: foo :: F PolyId\r
+    • Illegal polymorphic type: PolyId\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        foo :: F PolyId\r
index 0c7a062..cc84310 100644 (file)
@@ -1,20 +1,10 @@
-
-T8806.hs:5:6: error:
-    • Expected a constraint, but ‘Int’ has kind ‘*’
-    • In the type signature:
-        f :: Int => Int
-
-T8806.hs:8:7: error:
-    • Expected a constraint, but ‘Int’ has kind ‘*’
-    • In the type signature:
-        g :: (Int => Show a) => Int
-
-T8806.hs:8:7: error:
-    • Expected a constraint, but ‘Show a’ has kind ‘*’
-    • In the type signature:
-        g :: (Int => Show a) => Int
-
-T8806.hs:8:14: error:
-    • Expected a type, but ‘Show a’ has kind ‘Constraint’
-    • In the type signature:
-        g :: (Int => Show a) => Int
+\r
+T8806.hs:5:6: error:\r
+    • Expected a constraint, but ‘Int’ has kind ‘*’\r
+    • In the type signature:\r
+        f :: Int => Int\r
+\r
+T8806.hs:8:7: error:\r
+    • Expected a constraint, but ‘Int’ has kind ‘*’\r
+    • In the type signature:\r
+        g :: (Int => Show a) => Int\r
index c6765a9..7aa06b2 100644 (file)
@@ -1,15 +1,12 @@
-
-T9196.hs:4:7: error:
-    • Illegal constraint: forall a. Eq a
-    • In the type signature:
-        f :: (forall a. Eq a) => a -> a
-
-T9196.hs:7:7: error:
-    • Expected a constraint, but ‘Ord a’ has kind ‘*’
-    • In the type signature:
-        g :: (Eq a => Ord a) => a -> a
-
-T9196.hs:7:15: error:
-    • Expected a type, but ‘Ord a’ has kind ‘Constraint’
-    • In the type signature:
-        g :: (Eq a => Ord a) => a -> a
+\r
+T9196.hs:4:6: error:\r
+    • Illegal polymorphic type: forall a1. Eq a1\r
+      A constraint must be a monotype\r
+    • In the type signature:\r
+        f :: (forall a. Eq a) => a -> a\r
+\r
+T9196.hs:7:6: error:\r
+    • Illegal qualified type: Eq a => Ord a\r
+      A constraint must be a monotype\r
+    • In the type signature:\r
+        g :: (Eq a => Ord a) => a -> a\r
index 1aedd2a..04081ab 100644 (file)
@@ -1,4 +1,4 @@
-
-tcfail088.hs:9:19:
-    Illegal polymorphic or qualified type: forall s1. T s1 a
-    In the instance declaration for ‘Ord (forall s. T s a)’
+\r
+tcfail088.hs:9:19: error:\r
+    • Illegal polymorphic type: forall s. T s a\r
+    • In the instance declaration for ‘Ord (forall s. T s a)’\r
index feda55f..205bed8 100644 (file)
@@ -1,5 +1,6 @@
 \r
 tcfail127.hs:3:8: error:\r
-    Illegal polymorphic or qualified type: Num a => a -> a\r
-    GHC doesn't yet support impredicative polymorphism\r
-    In the type signature: foo :: IO (Num a => a -> a)\r
+    • Illegal qualified type: Num a => a -> a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        foo :: IO (Num a => a -> a)\r
index ed33280..ceb057f 100644 (file)
@@ -1,7 +1,6 @@
-
-tcfail184.hs:8:19:
-    Illegal polymorphic or qualified type:
-      forall a1. Ord a1 => [a1] -> [a1]
-    Perhaps you intended to use RankNTypes or Rank2Types
-    In the definition of data constructor ‘MkSwizzle’
-    In the newtype declaration for ‘Swizzle’
+\r
+tcfail184.hs:8:19: error:\r
+    • Illegal polymorphic type: forall a. Ord a => [a] -> [a]\r
+      Perhaps you intended to use RankNTypes or Rank2Types\r
+    • In the definition of data constructor ‘MkSwizzle’\r
+      In the newtype declaration for ‘Swizzle’\r
index c044a37..c328b73 100644 (file)
@@ -1,5 +1,5 @@
-
-tcfail195.hs:6:3: error:
-    Illegal polymorphic or qualified type: forall a1. a1
-    In the definition of data constructor ‘Foo’
-    In the data type declaration for ‘Foo’
+\r
+tcfail195.hs:6:3: error:\r
+    • Illegal polymorphic type: forall a. a\r
+    • In the definition of data constructor ‘Foo’\r
+      In the data type declaration for ‘Foo’\r
index 0dbbda8..e8cfd6b 100644 (file)
@@ -1,5 +1,6 @@
-
-tcfail196.hs:5:8: error:
-    • Illegal polymorphic or qualified type: forall a1. a1
-    • In the type signature:
-        bar :: Num (forall a. a) => Int -> Int
+\r
+tcfail196.hs:5:8: error:\r
+    • Illegal polymorphic type: forall a. a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        bar :: Num (forall a. a) => Int -> Int\r
index 802a77f..ba8be62 100644 (file)
@@ -1,6 +1,6 @@
-
-tcfail197.hs:5:8: error:
-    • Illegal polymorphic or qualified type: forall a1. a1
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        foo :: [forall a. a] -> Int
+\r
+tcfail197.hs:5:8: error:\r
+    • Illegal polymorphic type: forall a. a\r
+      GHC doesn't yet support impredicative polymorphism\r
+    • In the type signature:\r
+        foo :: [forall a. a] -> Int\r