fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla

Mon Sep 18 14:51:33 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla
  Sat Aug  5 21:48:21 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * fix some coercion kind representation things, extend exprIsConApp_maybe to non-vanilla
    Wed Jul 19 08:06:28 EDT 2006  kevind@bu.edu

diff --git a/compiler/Makefile b/compiler/Makefile
index 43622c3..e81ccfb 100644 (file)
--- a/compiler/Makefile
+++ b/compiler/Makefile
@@ -411,7 +411,7 @@ endif
 ifeq "$(GhcWithInterpreter) $(bootstrapped)" "YES YES"
 
 # Yes, include the interepreter, readline, and Template Haskell extensions
 ifeq "$(GhcWithInterpreter) $(bootstrapped)" "YES YES"
 
 # Yes, include the interepreter, readline, and Template Haskell extensions

-SRC_HC_OPTS += -DGHCI -DBREAKPOINT -package template-haskell
+SRC_HC_OPTS += -DGHCI -package template-haskell

 PKG_DEPENDS += template-haskell
 
 # Use threaded RTS with GHCi, so threads don't get blocked at the prompt.
 PKG_DEPENDS += template-haskell
 
 # Use threaded RTS with GHCi, so threads don't get blocked at the prompt.

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 0a1902e..1c25d81 100644 (file)
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -48,7 +48,7 @@ import TysWiredIn     ( charTy, mkListTy )
 import PrelRules       ( primOpRules )
 import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, newTyConInstRhs, coreEqType )
 import Coercion         ( mkSymCoercion, mkUnsafeCoercion, 
 import PrelRules       ( primOpRules )
 import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, newTyConInstRhs, coreEqType )
 import Coercion         ( mkSymCoercion, mkUnsafeCoercion, 

-                          splitRecNewTypeCo_maybe )
+                          splitNewTypeRepCo_maybe )

 import TcType          ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, 
                          mkTyConApp, mkTyVarTys, mkClassPred, 
                          mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, 
 import TcType          ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, 
                          mkTyConApp, mkTyVarTys, mkClassPred, 
                          mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, 

diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs
index 697f089..e4aa8c2 100644 (file)
--- a/compiler/basicTypes/Var.lhs
+++ b/compiler/basicTypes/Var.lhs
@@ -10,7 +10,7 @@ module Var (
        setVarName, setVarUnique, 
 
        -- TyVars
        setVarName, setVarUnique, 
 
        -- TyVars

-       TyVar, mkTyVar, mkTcTyVar,
+       TyVar, mkTyVar, mkTcTyVar, mkWildTyVar,

        tyVarName, tyVarKind,
        setTyVarName, setTyVarUnique, setTyVarKind,
        tcTyVarDetails,
        tyVarName, tyVarKind,
        setTyVarName, setTyVarUnique, setTyVarKind,
        tcTyVarDetails,

@@ -40,9 +40,10 @@ import {-# SOURCE #-}        TcType( TcTyVarDetails, pprTcTyVarDetails )
 import {-# SOURCE #-}  IdInfo( GlobalIdDetails, notGlobalId, IdInfo, seqIdInfo )
 
 import Name            ( Name, NamedThing(..),
 import {-# SOURCE #-}  IdInfo( GlobalIdDetails, notGlobalId, IdInfo, seqIdInfo )
 
 import Name            ( Name, NamedThing(..),

-                         setNameUnique, nameUnique
+                         setNameUnique, nameUnique, mkSysTvName

                        )
                        )

-import Unique          ( Unique, Uniquable(..), mkUniqueGrimily, getKey# )
+import Unique          ( Unique, Uniquable(..), mkUniqueGrimily, getKey#,
+                          mkBuiltinUnique )

 import FastTypes
 import Outputable
 \end{code}
 import FastTypes
 import Outputable
 \end{code}

@@ -197,6 +198,14 @@ mkTcTyVar name kind details
                tyVarKind  = kind,
                tcTyVarDetails = details
        }
                tyVarKind  = kind,
                tcTyVarDetails = details
        }

+
+mkWildTyVar :: Kind -> TyVar
+mkWildTyVar kind 
+  = TyVar { varName = mkSysTvName wild_uniq FSLIT("co_wild"),
+            realUnique = _ILIT(1),
+            tyVarKind = kind }
+  where
+    wild_uniq = (mkBuiltinUnique 1)

 \end{code}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************

diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index 9b58159..19a44dc 100644 (file)
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -42,7 +42,7 @@ import GLAEXTS                -- For `xori`
 import CoreSyn
 import CoreFVs         ( exprFreeVars )
 import PprCore         ( pprCoreExpr )
 import CoreSyn
 import CoreFVs         ( exprFreeVars )
 import PprCore         ( pprCoreExpr )

-import Var             ( Var, TyVar )
+import Var             ( Var, TyVar, isCoVar, tyVarKind )

 import VarSet          ( unionVarSet )
 import VarEnv
 import Name            ( hashName )
 import VarSet          ( unionVarSet )
 import VarEnv
 import Name            ( hashName )

@@ -53,7 +53,7 @@ import Literal                ( hashLiteral, literalType, litIsDupable,
                          litIsTrivial, isZeroLit, Literal( MachLabel ) )
 import DataCon         ( DataCon, dataConRepArity, 
                          isVanillaDataCon, dataConTyCon, dataConRepArgTys,
                          litIsTrivial, isZeroLit, Literal( MachLabel ) )
 import DataCon         ( DataCon, dataConRepArity, 
                          isVanillaDataCon, dataConTyCon, dataConRepArgTys,

-                          dataConUnivTyVars )
+                          dataConUnivTyVars, dataConExTyVars )

 import PrimOp          ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap )
 import Id              ( Id, idType, globalIdDetails, idNewStrictness, 
                          mkWildId, idArity, idName, idUnfolding, idInfo,
 import PrimOp          ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap )
 import Id              ( Id, idType, globalIdDetails, idNewStrictness, 
                          mkWildId, idArity, idName, idUnfolding, idInfo,

@@ -70,8 +70,9 @@ import Type           ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe,
                           substTyWith
                        )
 import Coercion         ( Coercion, mkTransCoercion, coercionKind,
                           substTyWith
                        )
 import Coercion         ( Coercion, mkTransCoercion, coercionKind,

-                          splitRecNewTypeCo_maybe, mkSymCoercion, mkLeftCoercion,
-                          mkRightCoercion, decomposeCo, coercionKindTyConApp )
+                          splitNewTypeRepCo_maybe, mkSymCoercion, mkLeftCoercion,
+                          mkRightCoercion, decomposeCo, coercionKindTyConApp,
+                          splitCoercionKind )

 import TyCon           ( tyConArity )
 import TysWiredIn      ( boolTy, trueDataCon, falseDataCon )
 import CostCentre      ( CostCentre )
 import TyCon           ( tyConArity )
 import TysWiredIn      ( boolTy, trueDataCon, falseDataCon )
 import CostCentre      ( CostCentre )

@@ -687,30 +688,62 @@ exprIsConApp_maybe (Cast expr co)
        --        (# r, s #) -> ...
        -- where the memcpy is in the IO monad, but the call is in
        -- the (ST s) monad
        --        (# r, s #) -> ...
        -- where the memcpy is in the IO monad, but the call is in
        -- the (ST s) monad

-    let (from_ty, to_ty) = coercionKind co in

     case exprIsConApp_maybe expr of {
        Nothing           -> Nothing ;
        Just (dc, args)   -> 
     case exprIsConApp_maybe expr of {
        Nothing           -> Nothing ;
        Just (dc, args)   -> 

+
+    let (from_ty, to_ty) = coercionKind co in

   
     case splitTyConApp_maybe to_ty of {
        Nothing -> Nothing ;
        Just (tc, tc_arg_tys) | tc /= dataConTyCon dc     -> Nothing
   
     case splitTyConApp_maybe to_ty of {
        Nothing -> Nothing ;
        Just (tc, tc_arg_tys) | tc /= dataConTyCon dc     -> Nothing

-                             | not (isVanillaDataCon dc) -> Nothing
+                           --  | not (isVanillaDataCon dc) -> Nothing

                              | otherwise                 ->
                              | otherwise                 ->

-               -- Type constructor must match
-               -- We knock out existentials to keep matters simple(r)
+               -- Type constructor must match datacon
+
+    case splitTyConApp_maybe from_ty of {
+        Nothing -> Nothing ;
+        Just (tc', tc_arg_tys') | tc /= tc' -> Nothing 
+                -- Both sides of coercion must have the same type constructor
+                               | otherwise ->
+

     let
     let

+        -- here we do the PushC reduction rule as described in the FC paper

        arity               = tyConArity tc
        arity               = tyConArity tc

-       val_args            = drop arity args
+        n_ex_tvs            = length dc_ex_tyvars
+
+        (univ_args, rest)   = splitAt arity args
+        (ex_args, val_args) = splitAt n_ex_tvs rest
+

         arg_tys            = dataConRepArgTys dc
        dc_tyvars           = dataConUnivTyVars dc
         arg_tys            = dataConRepArgTys dc
        dc_tyvars           = dataConUnivTyVars dc

+        dc_ex_tyvars        = dataConExTyVars dc
+

         deep arg_ty         = deepCast arg_ty dc_tyvars co
         deep arg_ty         = deepCast arg_ty dc_tyvars co

+
+          -- first we appropriately cast the value arguments
+        arg_cos             = map deep arg_tys 

        new_val_args        = zipWith mkCoerce (map deep arg_tys) val_args
        new_val_args        = zipWith mkCoerce (map deep arg_tys) val_args

+
+          -- then we cast the existential coercion arguments
+        orig_tvs            = dc_tyvars ++ dc_ex_tyvars
+        gammas              = decomposeCo arity co
+        new_tys             = gammas ++ (map (\ (Type t) -> t) ex_args)
+        theta               = substTyWith orig_tvs new_tys
+        cast_ty tv (Type ty) 
+          | isCoVar tv
+          , (ty1, ty2) <- splitCoercionKind (tyVarKind tv)
+          = Type $ mkTransCoercion (mkSymCoercion (theta ty1)) 
+            (mkTransCoercion ty (theta ty2))
+          | otherwise       
+          = Type ty
+        new_ex_args         = zipWith cast_ty dc_ex_tyvars ex_args
+  

     in
     ASSERT( all isTypeArg (take arity args) )
     ASSERT( equalLength val_args arg_tys )
     in
     ASSERT( all isTypeArg (take arity args) )
     ASSERT( equalLength val_args arg_tys )

-    Just (dc, map Type tc_arg_tys ++ new_val_args)
-    }}
+    Just (dc, map Type tc_arg_tys ++ new_ex_args ++ new_val_args)
+    }}}

 
 exprIsConApp_maybe (Note _ expr)
   = exprIsConApp_maybe expr
 
 exprIsConApp_maybe (Note _ expr)
   = exprIsConApp_maybe expr

@@ -1047,7 +1080,7 @@ eta_expand n us expr ty
                -- We want to get
                --      coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
 
                -- We want to get
                --      coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
 

-       case splitRecNewTypeCo_maybe ty of {
+       case splitNewTypeRepCo_maybe ty of {

          Just(ty1,co) -> 
               mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ;
          Nothing  -> 
          Just(ty1,co) -> 
               mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ;
          Nothing  -> 

diff --git a/compiler/deSugar/DsCCall.lhs b/compiler/deSugar/DsCCall.lhs
index 0541f5d..4fe5f2d 100644 (file)
--- a/compiler/deSugar/DsCCall.lhs
+++ b/compiler/deSugar/DsCCall.lhs
@@ -34,7 +34,7 @@ import Type           ( Type, isUnLiftedType, mkFunTys, mkFunTy,
                          splitRecNewType_maybe, splitForAllTy_maybe,
                          isUnboxedTupleType
                        )
                          splitRecNewType_maybe, splitForAllTy_maybe,
                          isUnboxedTupleType
                        )

-import Coercion         ( Coercion, splitRecNewTypeCo_maybe, mkSymCoercion )
+import Coercion         ( Coercion, splitNewTypeRepCo_maybe, mkSymCoercion )

 import PrimOp          ( PrimOp(..) )
 import TysPrim         ( realWorldStatePrimTy, intPrimTy,
                          byteArrayPrimTyCon, mutableByteArrayPrimTyCon,
 import PrimOp          ( PrimOp(..) )
 import TysPrim         ( realWorldStatePrimTy, intPrimTy,
                          byteArrayPrimTyCon, mutableByteArrayPrimTyCon,

@@ -160,7 +160,7 @@ unboxArg arg
   = returnDs (arg, \body -> body)
 
   -- Recursive newtypes
   = returnDs (arg, \body -> body)
 
   -- Recursive newtypes

-  | Just(rep_ty, co) <- splitRecNewTypeCo_maybe arg_ty
+  | Just(rep_ty, co) <- splitNewTypeRepCo_maybe arg_ty

   = unboxArg (mkCoerce (mkSymCoercion co) arg)
       
   -- Booleans
   = unboxArg (mkCoerce (mkSymCoercion co) arg)
       
   -- Booleans

@@ -399,7 +399,7 @@ resultWrapper result_ty
                                    (LitAlt (mkMachInt 0),[],Var falseDataConId)])
 
   -- Recursive newtypes
                                    (LitAlt (mkMachInt 0),[],Var falseDataConId)])
 
   -- Recursive newtypes

-  | Just (rep_ty, co) <- splitRecNewTypeCo_maybe result_ty
+  | Just (rep_ty, co) <- splitNewTypeRepCo_maybe result_ty

   = resultWrapper rep_ty `thenDs` \ (maybe_ty, wrapper) ->
     returnDs (maybe_ty, \e -> mkCoerce co (wrapper e))
 
   = resultWrapper rep_ty `thenDs` \ (maybe_ty, wrapper) ->
     returnDs (maybe_ty, \e -> mkCoerce co (wrapper e))
 

diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs
index 85b4b49..f9cc644 100644 (file)
--- a/compiler/simplCore/Simplify.lhs
+++ b/compiler/simplCore/Simplify.lhs
@@ -1696,7 +1696,7 @@ knownCon env scrut con args bndr alts cont
                                  simplExprF env rhs cont
 
        (DataAlt dc, bs, rhs)  
                                  simplExprF env rhs cont
 
        (DataAlt dc, bs, rhs)  

-               -> ASSERT( n_drop_tys + length bs == length args )
+               -> -- ASSERT( n_drop_tys + length bs == length args )

                   bind_args env dead_bndr bs (drop n_drop_tys args)    $ \ env ->
                   let
                        -- It's useful to bind bndr to scrut, rather than to a fresh
                   bind_args env dead_bndr bs (drop n_drop_tys args)    $ \ env ->
                   let
                        -- It's useful to bind bndr to scrut, rather than to a fresh

diff --git a/compiler/stranal/WwLib.lhs b/compiler/stranal/WwLib.lhs
index 5896785..386c9e1 100644 (file)
--- a/compiler/stranal/WwLib.lhs
+++ b/compiler/stranal/WwLib.lhs
@@ -23,7 +23,7 @@ import TysWiredIn     ( tupleCon )
 import Type            ( Type, isUnLiftedType, mkFunTys,
                          splitForAllTys, splitFunTys, splitRecNewType_maybe, isAlgType
                        )
 import Type            ( Type, isUnLiftedType, mkFunTys,
                          splitForAllTys, splitFunTys, splitRecNewType_maybe, isAlgType
                        )

-import Coercion         ( Coercion, mkSymCoercion, splitRecNewTypeCo_maybe )
+import Coercion         ( Coercion, mkSymCoercion, splitNewTypeRepCo_maybe )

 import BasicTypes      ( Boxity(..) )
 import Var              ( Var, isId )
 import UniqSupply      ( returnUs, thenUs, getUniquesUs, UniqSM )
 import BasicTypes      ( Boxity(..) )
 import Var              ( Var, isId )
 import UniqSupply      ( returnUs, thenUs, getUniquesUs, UniqSM )

@@ -225,7 +225,7 @@ mkWWargs :: Type
                     Type)                      -- Type of wrapper body
 
 mkWWargs fun_ty demands one_shots
                     Type)                      -- Type of wrapper body
 
 mkWWargs fun_ty demands one_shots

-  | Just (rep_ty, co) <- splitRecNewTypeCo_maybe fun_ty
+  | Just (rep_ty, co) <- splitNewTypeRepCo_maybe fun_ty

        -- The newtype case is for when the function has
        -- a recursive newtype after the arrow (rare)
        -- We check for arity >= 0 to avoid looping in the case
        -- The newtype case is for when the function has
        -- a recursive newtype after the arrow (rare)
        -- We check for arity >= 0 to avoid looping in the case

diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index bda4e2f..c0a9294 100644 (file)
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -54,7 +54,7 @@ import {- Kind parts of -}
 
 import Id              ( Id, idType, recordSelectorFieldLabel,
                          isRecordSelector, isNaughtyRecordSelector,
 
 import Id              ( Id, idType, recordSelectorFieldLabel,
                          isRecordSelector, isNaughtyRecordSelector,

-                         isDataConId_maybe )
+                         isDataConId_maybe, idName )

 import DataCon         ( DataCon, dataConFieldLabels, dataConStrictMarks,
                          dataConSourceArity, 
                          dataConWrapId, isVanillaDataCon, dataConUnivTyVars,
 import DataCon         ( DataCon, dataConFieldLabels, dataConStrictMarks,
                          dataConSourceArity, 
                          dataConWrapId, isVanillaDataCon, dataConUnivTyVars,

diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 55e20fc..727d0ab 100644 (file)
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -170,9 +170,10 @@ import Type                (       -- Re-exports
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
 import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
 import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )

+import Coercion         ( splitForAllCo_maybe )

 import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
 import Class           ( Class )
 import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
 import Class           ( Class )

-import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
+import Var             ( TyVar, Id, isCoVar, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )

 import ForeignCall     ( Safety, DNType(..) )
 import Unify           ( tcMatchTys )
 import VarSet
 import ForeignCall     ( Safety, DNType(..) )
 import Unify           ( tcMatchTys )
 import VarSet

@@ -642,7 +643,8 @@ tcSplitForAllTys :: Type -> ([TyVar], Type)
 tcSplitForAllTys ty = split ty ty []
    where
      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
 tcSplitForAllTys ty = split ty ty []
    where
      split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs

-     split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
+     split orig_ty (ForAllTy tv ty) tvs 
+       | not (isCoVar tv) = split ty ty (tv:tvs)

      split orig_ty t               tvs = (reverse tvs, orig_ty)
 
 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
      split orig_ty t               tvs = (reverse tvs, orig_ty)
 
 tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'

@@ -655,6 +657,8 @@ tcSplitPhiTy ty = split ty ty []
   split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
   split orig_ty (FunTy arg res) ts 
        | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
   split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
   split orig_ty (FunTy arg res) ts 
        | Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)

+  split orig_ty ty ts
+        | Just (p, ty') <- splitForAllCo_maybe ty = split ty' ty' (p:ts) 

   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)

diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index c3013ab..b7f521a 100644 (file)
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -24,7 +24,7 @@ module Type (
 
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
 
         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 

-        isCoSuperKind, isSuperKind, isCoercionKind,
+        isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,

        mkArrowKind, mkArrowKinds,
 
         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
        mkArrowKind, mkArrowKinds,
 
         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,

@@ -106,7 +106,7 @@ import TypeRep
 
 -- friends:
 import Var     ( Var, TyVar, tyVarKind, tyVarName, 
 
 -- friends:
 import Var     ( Var, TyVar, tyVarKind, tyVarName, 

-                 setTyVarName, setTyVarKind )
+                 setTyVarName, setTyVarKind, mkWildTyVar )

 import VarEnv
 import VarSet
 
 import VarEnv
 import VarSet
 

@@ -164,7 +164,9 @@ coreView :: Type -> Maybe Type
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
 coreView (NoteTy _ ty)            = Just ty
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
 coreView (NoteTy _ ty)            = Just ty

-coreView (PredTy p)               = Just (predTypeRep p)
+coreView (PredTy p)
+  | isEqPred p             = Nothing
+  | otherwise             = Just (predTypeRep p)

 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
                           = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
                                -- Its important to use mkAppTys, rather than (foldl AppTy),
 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
                           = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
                                -- Its important to use mkAppTys, rather than (foldl AppTy),

@@ -305,10 +307,11 @@ splitAppTys ty = split ty ty []
 
 \begin{code}
 mkFunTy :: Type -> Type -> Type
 
 \begin{code}
 mkFunTy :: Type -> Type -> Type

+mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildTyVar (PredTy (EqPred ty1 ty2))) res

 mkFunTy arg res = FunTy arg res
 
 mkFunTys :: [Type] -> Type -> Type
 mkFunTy arg res = FunTy arg res
 
 mkFunTys :: [Type] -> Type -> Type

-mkFunTys tys ty = foldr FunTy ty tys
+mkFunTys tys ty = foldr mkFunTy ty tys

 
 isFunTy :: Type -> Bool 
 isFunTy ty = isJust (splitFunTy_maybe ty)
 
 isFunTy :: Type -> Bool 
 isFunTy ty = isJust (splitFunTy_maybe ty)

@@ -596,6 +599,7 @@ predTypeRep (IParam _ ty)     = ty
 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
        -- Result might be a newtype application, but the consumer will
        -- look through that too if necessary
 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
        -- Result might be a newtype application, but the consumer will
        -- look through that too if necessary

+predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))

 \end{code}
 
 
 \end{code}
 
 

@@ -1423,6 +1427,8 @@ isSubKind :: Kind -> Kind -> Bool
 -- (k1 `isSubKind` k2) checks that k1 <: k2
 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
 isSubKind (FunTy a1 r1) (FunTy a2 r2)        = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
 -- (k1 `isSubKind` k2) checks that k1 <: k2
 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
 isSubKind (FunTy a1 r1) (FunTy a2 r2)        = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)

+isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
+  = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'

 isSubKind k1           k2                    = False
 
 eqKind :: Kind -> Kind -> Bool
 isSubKind k1           k2                    = False
 
 eqKind :: Kind -> Kind -> Bool

@@ -1465,4 +1471,8 @@ isCoercionKind :: Kind -> Bool
 isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
 isCoercionKind (PredTy (EqPred {}))     = True
 isCoercionKind other                    = False
 isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
 isCoercionKind (PredTy (EqPred {}))     = True
 isCoercionKind other                    = False

+
+isEqPred :: PredType -> Bool
+isEqPred (EqPred _ _) = True
+isEqPred other       = False

 \end{code}
 \end{code}