Parse and desugar equational constraints

- With -findexed-types, equational constraints can appear in contexts 
  wherever class predicates are allowed.
- The two argument types need to be boxed and rank 0.

compiler/deSugar/DsMeta.hs

@@ -398,6 +398,7 @@ repPred (HsClassP cls tys) = do
 			       tcon <- repTy (HsTyVar cls)
 			       tys1 <- repLTys tys
 			       repTapps tcon tys1
+repPred p@(HsEqualP _ _) = notHandled "Equational constraint" (ppr p)
 repPred p@(HsIParam _ _) = notHandled "Implicit parameter constraint" (ppr p)
 
 -- yield the representation of a list of types

compiler/hsSyn/HsTypes.lhs

@@ -102,7 +102,8 @@ type HsContext name = [LHsPred name]
 
 type LHsPred name = Located (HsPred name)
 
-data HsPred name = HsClassP name [LHsType name]
+data HsPred name = HsClassP name [LHsType name]		 -- class constraint
+		 | HsEqualP (LHsType name) (LHsType name)-- equality constraint
 		 | HsIParam (IPName name) (LHsType name)
 
 type LHsType name = Located (HsType name)
@@ -268,9 +269,6 @@ splitHsFunType other 	   	   = ([], other)
 %*									*
 %************************************************************************
 
-NB: these types get printed into interface files, so 
-    don't change the printing format lightly
-
 \begin{code}
 instance (OutputableBndr name) => Outputable (HsType name) where
     ppr ty = pprHsType ty
@@ -280,8 +278,13 @@ instance (Outputable name) => Outputable (HsTyVarBndr name) where
     ppr (KindedTyVar name kind) = pprHsTyVarBndr name kind
 
 instance OutputableBndr name => Outputable (HsPred name) where
-    ppr (HsClassP clas tys) = ppr clas <+> hsep (map (pprParendHsType.unLoc) tys)
-    ppr (HsIParam n ty)    = hsep [ppr n, dcolon, ppr ty]
+    ppr (HsClassP clas tys) = ppr clas <+> hsep (map pprLHsType tys)
+    ppr (HsEqualP t1 t2)    = hsep [pprLHsType t1, ptext SLIT("~"), 
+				    pprLHsType t2]
+    ppr (HsIParam n ty)     = hsep [ppr n, dcolon, ppr ty]
+
+pprLHsType :: OutputableBndr name => LHsType name -> SDoc
+pprLHsType = pprParendHsType . unLoc
 
 pprHsTyVarBndr :: Outputable name => name -> Kind -> SDoc
 pprHsTyVarBndr name kind | isLiftedTypeKind kind = ppr name

compiler/parser/Parser.y.pp

@@ -981,7 +981,8 @@ gentype :: { LHsType RdrName }
         : btype                         { $1 }
         | btype qtyconop gentype        { LL $ HsOpTy $1 $2 $3 }
         | btype tyvarop  gentype  	{ LL $ HsOpTy $1 $2 $3 }
- 	| btype '->' ctype		{ LL $ HsFunTy $1 $3 }
+ 	| btype '->'     ctype		{ LL $ HsFunTy $1 $3 }
+        | btype '~'      gentype  	{ LL $ HsPredTy (HsEqualP $1 $3) }
 
 btype :: { LHsType RdrName }
 	: btype atype			{ LL $ HsAppTy $1 $2 }

compiler/parser/RdrHsSyn.lhs

@@ -97,8 +97,9 @@ extractHsRhoRdrTyVars ctxt ty
 
 extract_lctxt ctxt acc = foldr (extract_pred . unLoc) acc (unLoc ctxt)
 
-extract_pred (HsClassP cls tys) acc	= foldr extract_lty acc tys
-extract_pred (HsIParam n ty) acc	= extract_lty ty acc
+extract_pred (HsClassP cls tys) acc = foldr extract_lty acc tys
+extract_pred (HsEqualP ty1 ty2) acc = extract_lty ty1 (extract_lty ty2 acc)
+extract_pred (HsIParam n ty   ) acc = extract_lty ty acc
 
 extract_lty (L loc ty) acc 
   = case ty of
@@ -406,6 +407,15 @@ checkInstType (L l t)
 	ty ->   do dict_ty <- checkDictTy (L l ty)
 	      	   return (L l (HsForAllTy Implicit [] (noLoc []) dict_ty))
 
+checkDictTy :: LHsType RdrName -> P (LHsType RdrName)
+checkDictTy (L spn ty) = check ty []
+  where
+  check (HsTyVar t) args | not (isRdrTyVar t) 
+  	= return (L spn (HsPredTy (HsClassP t args)))
+  check (HsAppTy l r) args = check (unLoc l) (r:args)
+  check (HsParTy t)   args = check (unLoc t) args
+  check _ _ = parseError spn "Malformed instance header"
+
 -- Check whether the given list of type parameters are all type variables
 -- (possibly with a kind signature).  If the second argument is `False',
 -- only type variables are allowed and we raise an error on encountering a
@@ -477,10 +487,12 @@ checkTyClHdr (L l cxt) ty
     go l other	         acc    = 
       parseError l "Malformed head of type or class declaration"
 
-	-- The predicates in a type or class decl must all
-	-- be HsClassPs.  They need not all be type variables,
-	-- even in Haskell 98.  E.g. class (Monad m, Monad (t m)) => MonadT t m
-    chk_pred (L l (HsClassP _ args)) = return ()
+	-- The predicates in a type or class decl must be class predicates or 
+	-- equational constraints.  They need not all have variable-only
+	-- arguments, even in Haskell 98.  
+	-- E.g. class (Monad m, Monad (t m)) => MonadT t m
+    chk_pred (L l (HsClassP _ _)) = return ()
+    chk_pred (L l (HsEqualP _ _)) = return ()
     chk_pred (L l _)
        = parseError l "Malformed context in type or class declaration"
 
@@ -571,22 +583,16 @@ checkPred (L spn ty)
   where
     checkl (L l ty) args = check l ty args
 
+    check _loc (HsPredTy pred@(HsEqualP _ _)) 
+                                       args | null args
+					    = return $ L spn pred
     check _loc (HsTyVar t)             args | not (isRdrTyVar t) 
 		 		  	    = return (L spn (HsClassP t args))
     check _loc (HsAppTy l r)           args = checkl l (r:args)
     check _loc (HsOpTy l (L loc tc) r) args = check loc (HsTyVar tc) (l:r:args)
     check _loc (HsParTy t)  	       args = checkl t args
-    check loc _                        _    = parseError loc  "malformed class assertion"
-
-checkDictTy :: LHsType RdrName -> P (LHsType RdrName)
-checkDictTy (L spn ty) = check ty []
-  where
-  check (HsTyVar t) args | not (isRdrTyVar t) 
-  	= return (L spn (HsPredTy (HsClassP t args)))
-  check (HsAppTy l r) args = check (unLoc l) (r:args)
-  check (HsParTy t)   args = check (unLoc t) args
-  check _ _ = parseError spn "Malformed context in instance header"
-
+    check loc _                        _    = parseError loc  
+					        "malformed class assertion"
 
 ---------------------------------------------------------------------------
 -- Checking stand-alone deriving declarations

compiler/rename/RnHsSyn.lhs

@@ -87,6 +87,8 @@ extractHsCtxtTyNames (L _ ctxt)
 -- so don't mention the IP names
 extractHsPredTyNames (HsClassP cls tys)
   = unitNameSet cls `unionNameSets` extractHsTyNames_s tys
+extractHsPredTyNames (HsEqualP ty1 ty2)
+  = extractHsTyNames ty1 `unionNameSets` extractHsTyNames ty2
 extractHsPredTyNames (HsIParam n ty)
   = extractHsTyNames ty
 \end{code}

compiler/rename/RnTypes.lhs

@@ -505,14 +505,20 @@ rnLPred :: SDoc -> LHsPred RdrName -> RnM (LHsPred Name)
 rnLPred doc  = wrapLocM (rnPred doc)
 
 rnPred doc (HsClassP clas tys)
-  = lookupOccRn clas		`thenM` \ clas_name ->
-    rnLHsTypes doc tys		`thenM` \ tys' ->
-    returnM (HsClassP clas_name tys')
-
+  = do { clas_name <- lookupOccRn clas
+       ; tys' <- rnLHsTypes doc tys
+       ; returnM (HsClassP clas_name tys')
+       }
+rnPred doc (HsEqualP ty1 ty2)
+  = do { ty1' <- rnLHsType doc ty1
+       ; ty2' <- rnLHsType doc ty2
+       ; returnM (HsEqualP ty1' ty2')
+       }
 rnPred doc (HsIParam n ty)
-  = newIPNameRn n		`thenM` \ name ->
-    rnLHsType doc ty		`thenM` \ ty' ->
-    returnM (HsIParam name ty')
+  = do { name <- newIPNameRn n
+       ; ty' <- rnLHsType doc ty
+       ; returnM (HsIParam name ty')
+       }
 \end{code}
 
 

compiler/typecheck/TcHsType.lhs

@@ -388,13 +388,21 @@ kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
 	-- Does *not* check for a saturated
 	-- application (reason: used from TcDeriv)
 kc_pred pred@(HsIParam name ty)
-  = kcHsType ty		`thenM` \ (ty', kind) ->
-    returnM (HsIParam name ty', kind)
-
+  = do { (ty', kind) <- kcHsType ty
+       ; returnM (HsIParam name ty', kind)
+       }
 kc_pred pred@(HsClassP cls tys)
-  = kcClass cls			`thenM` \ kind ->
-    kcApps kind (ppr cls) tys	`thenM` \ (tys', res_kind) ->
-    returnM (HsClassP cls tys', res_kind)
+  = do { kind <- kcClass cls
+       ; (tys', res_kind) <- kcApps kind (ppr cls) tys
+       ; returnM (HsClassP cls tys', res_kind)
+       }
+kc_pred pred@(HsEqualP ty1 ty2)
+  = do { (ty1', kind1) <- kcHsType ty1
+       ; checkExpectedKind ty1 kind1 liftedTypeKind
+       ; (ty2', kind2) <- kcHsType ty2
+       ; checkExpectedKind ty2 kind2 liftedTypeKind
+       ; returnM (HsEqualP ty1 ty2, liftedTypeKind)
+       }
 
 ---------------------------
 kcTyVar :: Name -> TcM TcKind
@@ -534,13 +542,19 @@ dsHsLPred :: LHsPred Name -> TcM PredType
 dsHsLPred pred = dsHsPred (unLoc pred)
 
 dsHsPred pred@(HsClassP class_name tys)
-  = dsHsTypes tys			`thenM` \ arg_tys ->
-    tcLookupClass class_name		`thenM` \ clas ->
-    returnM (ClassP clas arg_tys)
-
+  = do { arg_tys <- dsHsTypes tys
+       ; clas <- tcLookupClass class_name
+       ; returnM (ClassP clas arg_tys)
+       }
+dsHsPred pred@(HsEqualP ty1 ty2)
+  = do { arg_ty1 <- dsHsType ty1
+       ; arg_ty2 <- dsHsType ty2
+       ; returnM (EqPred arg_ty1 arg_ty2)
+       }
 dsHsPred (HsIParam name ty)
-  = dsHsType ty					`thenM` \ arg_ty ->
-    returnM (IParam name arg_ty)
+  = do { arg_ty <- dsHsType ty
+       ; returnM (IParam name arg_ty)
+       }
 \end{code}
 
 GADT constructor signatures

compiler/typecheck/TcMType.lhs

@@ -924,14 +924,14 @@ check_valid_theta ctxt theta
 
 -------------------------
 check_pred_ty dflags ctxt pred@(ClassP cls tys)
-  = 	-- Class predicates are valid in all contexts
-    checkTc (arity == n_tys) arity_err		`thenM_`
-
-	-- Check the form of the argument types
-    mappM_ check_arg_type tys				`thenM_`
-    checkTc (check_class_pred_tys dflags ctxt tys)
-	    (predTyVarErr pred $$ how_to_allow)
-
+  = do {	-- Class predicates are valid in all contexts
+       ; checkTc (arity == n_tys) arity_err
+
+		-- Check the form of the argument types
+       ; mappM_ check_arg_type tys
+       ; checkTc (check_class_pred_tys dflags ctxt tys)
+		 (predTyVarErr pred $$ how_to_allow)
+       }
   where
     class_name = className cls
     arity      = classArity cls
@@ -939,10 +939,23 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     arity_err  = arityErr "Class" class_name arity n_tys
     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+  = do {	-- Equational constraints are valid in all contexts if indexed
+		-- types are permitted
+       ; checkTc (dopt Opt_IndexedTypes dflags) (eqPredTyErr pred)
+
+		-- Check the form of the argument types
+       ; check_eq_arg_type ty1
+       ; check_eq_arg_type ty2
+       }
+  where 
+    check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
+
 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-	-- Implicit parameters only allows in type
+	-- Implicit parameters only allowed in type
 	-- signatures; not in instance decls, superclasses etc
-	-- The reason for not allowing implicit params in instances is a bit subtle
+	-- The reason for not allowing implicit params in instances is a bit
+	-- subtle.
 	-- If we allowed	instance (?x::Int, Eq a) => Foo [a] where ...
 	-- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
 	-- discharge all the potential usas of the ?x in e.   For example, a
@@ -1057,6 +1070,9 @@ checkThetaCtxt ctxt theta
 	  ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+		   $$
+		   parens (ptext SLIT("Use -findexed-types to permit this"))
 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
 			  nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)

compiler/typecheck/TcType.lhs

@@ -59,7 +59,7 @@ module TcType (
 
   ---------------------------------
   -- Misc type manipulators
-  deNoteType, classesOfTheta,
+  deNoteType,
   tyClsNamesOfType, tyClsNamesOfDFunHead, 
   getDFunTyKey,
 
@@ -540,7 +540,7 @@ mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 
 mkPhiTy :: [PredType] -> Type -> Type
-mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
+mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
 \end{code}
 
 @isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
@@ -850,7 +850,8 @@ isInheritablePred :: PredType -> Bool
 -- but it doesn't need to be quantified over the Num a dictionary
 -- which can be free in g's rhs, and shared by both calls to g
 isInheritablePred (ClassP _ _) = True
-isInheritablePred other	     = False
+isInheritablePred (EqPred _ _) = True
+isInheritablePred other	       = False
 \end{code}
 
 --------------------- Equality predicates ---------------------------------
@@ -1043,10 +1044,6 @@ tyClsNamesOfDFunHead :: Type -> NameSet
 tyClsNamesOfDFunHead dfun_ty 
   = case tcSplitSigmaTy dfun_ty of
 	(tvs,_,head_ty) -> tyClsNamesOfType head_ty
-
-classesOfTheta :: ThetaType -> [Class]
--- Looks just for ClassP things; maybe it should check
-classesOfTheta preds = [ c | ClassP c _ <- preds ]
 \end{code}