[project @ 2003-06-20 11:14:18 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index dbf52a6..f3e864c 100644 (file)
@@ -16,49 +16,55 @@ is the principal client.
 \begin{code}
 module TcType (
   --------------------------------
+  -- TyThing
+  TyThing(..), -- instance NamedThing
+
+  --------------------------------
   -- Types 
-  TcType, TcTauType, TcPredType, TcThetaType, TcRhoType,
-  TcTyVar, TcTyVarSet, TcKind,
+  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, 
+  TcTyVar, TcTyVarSet, TcKind, 
 
   --------------------------------
   -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar,
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar, 
+  tyVarBindingInfo,
 
   --------------------------------
   -- Builders
-  mkRhoTy, mkSigmaTy, 
+  mkPhiTy, mkSigmaTy, 
 
   --------------------------------
   -- Splitters  
   -- These are important because they do not look through newtypes
-  tcSplitForAllTys, tcSplitRhoTy, 
+  tcSplitForAllTys, tcSplitPhiTy, 
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
-  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
-  isQualifiedTy, isOverloadedTy, 
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+  isSigmaTy, isOverloadedTy, 
   isDoubleTy, isFloatTy, isIntTy,
-  isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
+  isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  allDistinctTyVars,
 
   ---------------------------------
   -- Misc type manipulators
-  hoistForAllTys, deNoteType,
-  namesOfType, namesOfDFunHead,
+  deNoteType, classNamesOfTheta,
+  tyClsNamesOfType, tyClsNamesOfDFunHead, 
   getDFunTyKey,
 
   ---------------------------------
   -- Predicate types  
-  PredType, getClassPredTys_maybe, getClassPredTys, 
-  isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
-  mkDictTy, tcSplitPredTy_maybe, predTyUnique,
+  getClassPredTys_maybe, getClassPredTys, 
+  isPredTy, isClassPred, isTyVarClassPred, 
+  mkDictTy, tcSplitPredTy_maybe, 
   isDictTy, tcSplitDFunTy, predTyUnique, 
-  mkClassPred, inheritablePred, isIPPred, mkPredName,
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
   -- Foreign import and export
@@ -69,11 +75,14 @@ module TcType (
   isFFIDynArgumentTy,  -- :: Type -> Bool
   isFFIDynResultTy,    -- :: Type -> Bool
   isFFILabelTy,        -- :: Type -> Bool
+  isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
+  isFFIDotnetObjTy,    -- :: Type -> Bool
+  
+  toDNType,            -- :: Type -> DNType
 
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
@@ -81,21 +90,21 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind,
+  isTypeKind, isAnyTypeKind,
 
   Type, SourceType(..), PredType, ThetaType, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
-  mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
-  isPrimitiveType,
+  isPrimitiveType, isTyVarTy,
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
-  typeKind, eqKind, eqUsage,
+  typeKind, eqKind,
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
   ) where
@@ -104,42 +113,53 @@ module TcType (
 
 
 import {-# SOURCE #-} PprType( pprType )
+-- PprType imports TcType so that it can print intelligently
 
 -- friends:
 import TypeRep         ( Type(..), TyNote(..), funTyCon )  -- friend
-import Type            ( mkUTyM, unUTy )       -- Used locally
 
 import Type            (       -- Re-exports
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
-                         Kind, Type, TauType, SourceType(..), PredType, ThetaType, 
-                         unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
-                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
-                         mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
-                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
-                         isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
-                         splitNewType_maybe, splitTyConApp_maybe,
-                         tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-                         tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
-                         hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
+                         tyVarsOfTheta, Kind, Type, SourceType(..),
+                         PredType, ThetaType, unliftedTypeKind,
+                         liftedTypeKind, openTypeKind, mkArrowKind,
+                         mkArrowKinds, mkForAllTy, mkForAllTys,
+                         defaultKind, isTypeKind, isAnyTypeKind,
+                         mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
+                         mkTyConApp, mkGenTyConApp, mkAppTy,
+                         mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
+                         mkPredTys, isUnLiftedType,
+                         isUnboxedTupleType, isPrimitiveType,
+                         splitTyConApp_maybe,
+                         tidyTopType, tidyType, tidyPred, tidyTypes,
+                         tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
+                         tidyTyVarBndr, tidyOpenTyVar,
+                         tidyOpenTyVars, eqKind, 
+                         hasMoreBoxityInfo, liftedBoxity,
+                         superBoxity, typeKind, superKind, repType
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon )
+import DataCon         ( DataCon )
+import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
 import Class           ( classHasFDs, Class )
-import Var             ( TyVar, tyVarKind )
-import ForeignCall     ( Safety, playSafe )
+import Var             ( TyVar, Id, tyVarKind, isMutTyVar, mutTyVarDetails )
+import ForeignCall     ( Safety, playSafe
+                         , DNType(..)
+                       )
 import VarEnv
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkLocalName )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import OccName         ( OccName, mkDictOcc )
 import NameSet
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
-import TysWiredIn      ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
+import BasicTypes      ( IPName(..), ipNameName )
 import Unique          ( Unique, Uniquable(..) )
 import SrcLoc          ( SrcLoc )
-import Util            ( cmpList, thenCmp, equalLength )
+import Util            ( cmpList, thenCmp, equalLength, snocView )
 import Maybes          ( maybeToBool, expectJust )
 import Outputable
 \end{code}
@@ -147,10 +167,66 @@ import Outputable
 
 %************************************************************************
 %*                                                                     *
+                       TyThing
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+data TyThing = AnId     Id
+            | ADataCon DataCon
+            | ATyCon   TyCon
+            | AClass   Class
+
+instance NamedThing TyThing where
+  getName (AnId id)     = getName id
+  getName (ATyCon tc)   = getName tc
+  getName (AClass cl)   = getName cl
+  getName (ADataCon dc) = getName dc
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection{Types}
 %*                                                                     *
 %************************************************************************
 
+The type checker divides the generic Type world into the 
+following more structured beasts:
+
+sigma ::= forall tyvars. phi
+       -- A sigma type is a qualified type
+       --
+       -- Note that even if 'tyvars' is empty, theta
+       -- may not be: e.g.   (?x::Int) => Int
+
+       -- Note that 'sigma' is in prenex form:
+       -- all the foralls are at the front.
+       -- A 'phi' type has no foralls to the right of
+       -- an arrow
+
+phi :: theta => rho
+
+rho ::= sigma -> rho
+     |  tau
+
+-- A 'tau' type has no quantification anywhere
+-- Note that the args of a type constructor must be taus
+tau ::= tyvar
+     |  tycon tau_1 .. tau_n
+     |  tau_1 tau_2
+     |  tau_1 -> tau_2
+
+-- In all cases, a (saturated) type synonym application is legal,
+-- provided it expands to the required form.
+
+
+\begin{code}
+type SigmaType = Type
+type RhoType   = Type
+type TauType   = Type
+\end{code}
+
 \begin{code}
 type TcTyVar    = TyVar                -- Might be a mutable tyvar
 type TcTyVarSet = TyVarSet
@@ -163,8 +239,9 @@ type TcType = Type          -- A TcType can have mutable type variables
 
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
-type TcRhoType      = Type
-type TcTauType      = TauType
+type TcSigmaType    = TcType
+type TcRhoType      = TcType
+type TcTauType      = TcType
 type TcKind         = TcType
 \end{code}
 
@@ -177,6 +254,8 @@ type TcKind         = TcType
 
 TyVarDetails gives extra info about type variables, used during type
 checking.  It's attached to mutable type variables only.
+It's knot-tied back to Var.lhs.  There is no reason in principle
+why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
 \begin{code}
 data TyVarDetails
@@ -200,20 +279,31 @@ data TyVarDetails
 
    | VanillaTv -- Everything else
 
-isUserTyVar :: TyVarDetails -> Bool    -- Avoid unifying these if possible
-isUserTyVar VanillaTv = False
-isUserTyVar other     = True
-
-isSkolemTyVar :: TyVarDetails -> Bool
-isSkolemTyVar SigTv = True
-isSkolemTyVar other = False
-
-instance Outputable TyVarDetails where
-  ppr SigTv    = ptext SLIT("type signature")
-  ppr ClsTv     = ptext SLIT("class declaration")
-  ppr InstTv    = ptext SLIT("instance declaration")
-  ppr PatSigTv  = ptext SLIT("pattern type signature")
-  ppr VanillaTv = ptext SLIT("???")
+isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
+isUserTyVar tv = case mutTyVarDetails tv of
+                  VanillaTv -> False
+                  other     -> True
+
+isSkolemTyVar :: TcTyVar -> Bool
+isSkolemTyVar tv = case mutTyVarDetails tv of
+                     SigTv  -> True
+                     ClsTv  -> True
+                     InstTv -> True
+                     oteher -> False
+
+tyVarBindingInfo :: TyVar -> SDoc      -- Used in checkSigTyVars
+tyVarBindingInfo tv
+  | isMutTyVar tv
+  = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
+        ptext SLIT("at") <+> ppr (getSrcLoc tv)]
+  | otherwise
+  = empty
+  where
+    details SigTv     = ptext SLIT("type signature")
+    details ClsTv     = ptext SLIT("class declaration")
+    details InstTv    = ptext SLIT("instance declaration")
+    details PatSigTv  = ptext SLIT("pattern type signature")
+    details VanillaTv = ptext SLIT("//vanilla//")      -- Ditto
 \end{code}
 
 
@@ -224,12 +314,10 @@ instance Outputable TyVarDetails where
 %************************************************************************
 
 \begin{code}
-mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
-
-mkRhoTy :: [SourceType] -> Type -> Type
-mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
-                   foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
 
+mkPhiTy :: [SourceType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
 \end{code}
 
 
@@ -243,7 +331,6 @@ isTauTy (AppTy a b)  = isTauTy a && isTauTy b
 isTauTy (FunTy a b)     = isTauTy a && isTauTy b
 isTauTy (SourceTy p)    = True         -- Don't look through source types
 isTauTy (NoteTy _ ty)   = isTauTy ty
-isTauTy (UsageTy _ ty)   = isTauTy ty
 isTauTy other           = False
 \end{code}
 
@@ -256,7 +343,6 @@ getDFunTyKey (AppTy fun _)               = getDFunTyKey fun
 getDFunTyKey (NoteTy _ t)           = getDFunTyKey t
 getDFunTyKey (FunTy arg _)          = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)         = getDFunTyKey t
-getDFunTyKey (UsageTy _ t)          = getDFunTyKey t
 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc   -- Newtypes are quite reasonable
 getDFunTyKey ty                             = pprPanic "getDFunTyKey" (pprType ty)
 -- SourceTy shouldn't happen
@@ -283,26 +369,23 @@ tcSplitForAllTys ty = split ty ty []
    where
      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
-     split orig_ty (UsageTy _ ty)   tvs = split orig_ty ty tvs
      split orig_ty t               tvs = (reverse tvs, orig_ty)
 
 tcIsForAllTy (ForAllTy tv ty) = True
 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
-tcIsForAllTy (UsageTy n ty)   = tcIsForAllTy ty
 tcIsForAllTy t               = False
 
-tcSplitRhoTy :: Type -> ([PredType], Type)
-tcSplitRhoTy ty = split ty ty []
+tcSplitPhiTy :: Type -> ([PredType], Type)
+tcSplitPhiTy ty = split ty ty []
  where
   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
                                        Just p  -> split res res (p:ts)
                                        Nothing -> (reverse ts, orig_ty)
   split orig_ty (NoteTy n ty)  ts = split orig_ty ty ts
-  split orig_ty (UsageTy _ ty)  ts = split orig_ty ty ts
   split orig_ty ty             ts = (reverse ts, orig_ty)
 
 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
-                       (tvs, rho) -> case tcSplitRhoTy rho of
+                       (tvs, rho) -> case tcSplitPhiTy rho of
                                        (theta, tau) -> (tvs, theta, tau)
 
 tcTyConAppTyCon :: Type -> TyCon
@@ -317,12 +400,11 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                        Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
--- Newtypes are opaque, so they may be split
 tcSplitTyConApp_maybe (TyConApp tc tys)        = Just (tc, tys)
-tcSplitTyConApp_maybe (FunTy arg res)          = Just (funTyCon, [unUTy arg,unUTy res])
+tcSplitTyConApp_maybe (FunTy arg res)          = Just (funTyCon, [arg,res])
 tcSplitTyConApp_maybe (NoteTy n ty)            = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (UsageTy _ ty)           = tcSplitTyConApp_maybe ty
 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+       -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
@@ -337,7 +419,6 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
-tcSplitFunTy_maybe (UsageTy _ ty)   = tcSplitFunTy_maybe ty
 tcSplitFunTy_maybe other           = Nothing
 
 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
@@ -345,29 +426,32 @@ tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 
 
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitAppTy_maybe (FunTy ty1 ty2)          = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
+tcSplitAppTy_maybe (FunTy ty1 ty2)          = Just (TyConApp funTyCon [ty1], ty2)
 tcSplitAppTy_maybe (AppTy ty1 ty2)          = Just (ty1, ty2)
 tcSplitAppTy_maybe (NoteTy n ty)            = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (UsageTy _ ty)           = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
-       --- Don't forget that newtype!
+tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys     --- Don't forget that newtype!
 tcSplitAppTy_maybe (TyConApp tc tys)        = tc_split_app tc tys
 tcSplitAppTy_maybe other                    = Nothing
 
-tc_split_app tc []  = Nothing
-tc_split_app tc tys = split tys []
-                   where
-                     split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
-                     split (ty:tys) acc = split tys (ty:acc)
+tc_split_app tc tys = case snocView tys of
+                       Just (tys',ty') -> Just (TyConApp tc tys', ty')
+                       Nothing         -> Nothing
 
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
                    Just stuff -> stuff
                    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 
+tcSplitAppTys :: Type -> (Type, [Type])
+tcSplitAppTys ty
+  = go ty []
+  where
+    go ty args = case tcSplitAppTy_maybe ty of
+                  Just (ty', arg) -> go ty' (arg:args)
+                  Nothing         -> (ty,args)
+
 tcGetTyVar_maybe :: Type -> Maybe TyVar
 tcGetTyVar_maybe (TyVarTy tv)  = Just tv
 tcGetTyVar_maybe (NoteTy _ t)  = tcGetTyVar_maybe t
-tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
 tcGetTyVar_maybe other         = Nothing
 
 tcGetTyVar :: String -> Type -> TyVar
@@ -382,8 +466,7 @@ The type of a method for class C is always of the form:
 where sig_ty is the type given by the method's signature, and thus in general
 is a ForallTy.  At the point that splitMethodTy is called, it is expected
 that the outer Forall has already been stripped off.  splitMethodTy then
-returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
-Usages stripped off.
+returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
 
 \begin{code}
 tcSplitMethodTy :: Type -> (PredType, Type)
@@ -393,7 +476,6 @@ tcSplitMethodTy ty = split ty
                            Just p  -> (p, res)
                            Nothing -> panic "splitMethodTy"
   split (NoteTy n ty)  = split ty
-  split (UsageTy _ ty)  = split ty
   split _               = panic "splitMethodTy"
 
 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
@@ -404,6 +486,31 @@ tcSplitDFunTy ty
     (tvs, theta, clas, tys) }}
 \end{code}
 
+(allDistinctTyVars tys tvs) = True 
+       iff 
+all the types tys are type variables, 
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables.  For example, if the type sig is
+       f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't 
+       (a) been unified with a non-tyvar type
+       (b) been unified with each other (all distinct)
+       (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars []       acc
+  = True
+allDistinctTyVars (ty:tys) acc 
+  = case tcGetTyVar_maybe ty of
+       Nothing                       -> False  -- (a)
+       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
+               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}    
+
 
 %************************************************************************
 %*                                                                     *
@@ -417,42 +524,33 @@ tcSplitDFunTy ty
 isPred :: SourceType -> Bool
 isPred (ClassP _ _) = True
 isPred (IParam _ _) = True
-isPred (NType _ __) = False
+isPred (NType _ _)  = False
 
 isPredTy :: Type -> Bool
 isPredTy (NoteTy _ ty)  = isPredTy ty
-isPredTy (UsageTy _ ty) = isPredTy ty
 isPredTy (SourceTy sty) = isPred sty
 isPredTy _             = False
 
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
 tcSplitPredTy_maybe (NoteTy _ ty)          = tcSplitPredTy_maybe ty
-tcSplitPredTy_maybe (UsageTy _ ty)         = tcSplitPredTy_maybe ty
 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 tcSplitPredTy_maybe other                  = Nothing
        
 predTyUnique :: PredType -> Unique
-predTyUnique (IParam n _)      = getUnique n
+predTyUnique (IParam n _)      = getUnique (ipNameName n)
 predTyUnique (ClassP clas tys) = getUnique clas
 
-predHasFDs :: PredType -> Bool
--- True if the predicate has functional depenencies; 
--- I.e. should participate in improvement
-predHasFDs (IParam _ _)   = True
-predHasFDs (ClassP cls _) = classHasFDs cls
-
 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
-mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam name ty) = name
+mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
+mkPredName uniq loc (IParam ip ty)   = mkInternalName uniq (getOccName (ipNameName ip)) loc
 \end{code}
 
 
 --------------------- Dictionary types ---------------------------------
 
 \begin{code}
-mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
-                       ClassP clas tys
+mkClassPred clas tys = ClassP clas tys
 
 isClassPred :: SourceType -> Bool
 isClassPred (ClassP clas tys) = True
@@ -469,13 +567,11 @@ getClassPredTys :: PredType -> (Class, [Type])
 getClassPredTys (ClassP clas tys) = (clas, tys)
 
 mkDictTy :: Class -> [Type] -> Type
-mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
-                    mkPredTy (ClassP clas tys)
+mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
 isDictTy :: Type -> Bool
 isDictTy (SourceTy p)   = isClassPred p
 isDictTy (NoteTy _ ty) = isDictTy ty
-isDictTy (UsageTy _ ty) = isDictTy ty
 isDictTy other         = False
 \end{code}
 
@@ -486,7 +582,7 @@ isIPPred :: SourceType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
-inheritablePred :: PredType -> Bool
+isInheritablePred :: PredType -> Bool
 -- Can be inherited by a context.  For example, consider
 --     f x = let g y = (?v, y+x)
 --           in (g 3 with ?v = 8, 
@@ -495,8 +591,12 @@ inheritablePred :: PredType -> Bool
 --     g :: (?v :: a) => a -> a
 -- 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
-inheritablePred (ClassP _ _) = True
-inheritablePred other       = False
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other             = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other                = False
 \end{code}
 
 
@@ -513,6 +613,9 @@ But ignoring usage types
 tcEqType :: Type -> Type -> Bool
 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
+
 tcEqPred :: PredType -> PredType -> Bool
 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 
@@ -532,11 +635,9 @@ cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
   -- we in effect substitute tv2 for tv1 in t1 before continuing
 
-    -- Look through NoteTy and UsageTy
+    -- Look through NoteTy
 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
 
     -- Deal with equal constructors
 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
@@ -571,7 +672,7 @@ cmpTy env _ _ = LT
 
 \begin{code}
 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
-cmpSourceTy env (IParam n1 ty1)   (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
        -- Compare types as well as names for implicit parameters
        -- This comparison is used exclusively (I think) for the
        -- finite map built in TcSimplify
@@ -600,30 +701,27 @@ instance Ord SourceType where { compare = tcCmpPred }
 %*                                                                     *
 %************************************************************************
 
-isQualifiedTy returns true of any qualified type.  It doesn't *necessarily* have 
+isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have 
 any foralls.  E.g.
        f :: (?x::Int) => Int -> Int
 
 \begin{code}
-isQualifiedTy :: Type -> Bool
-isQualifiedTy (ForAllTy tyvar ty) = True
-isQualifiedTy (FunTy a b)        = isPredTy a
-isQualifiedTy (NoteTy n ty)      = isQualifiedTy ty
-isQualifiedTy (UsageTy _ ty)     = isQualifiedTy ty
-isQualifiedTy _                          = False
+isSigmaTy :: Type -> Bool
+isSigmaTy (ForAllTy tyvar ty) = True
+isSigmaTy (FunTy a b)        = isPredTy a
+isSigmaTy (NoteTy n ty)              = isSigmaTy ty
+isSigmaTy _                  = False
 
 isOverloadedTy :: Type -> Bool
 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 isOverloadedTy (FunTy a b)        = isPredTy a
 isOverloadedTy (NoteTy n ty)      = isOverloadedTy ty
-isOverloadedTy (UsageTy _ ty)     = isOverloadedTy ty
 isOverloadedTy _                  = False
 \end{code}
 
 \begin{code}
 isFloatTy      = is_tc floatTyConKey
 isDoubleTy     = is_tc doubleTyConKey
-isForeignPtrTy = is_tc foreignPtrTyConKey
 isIntegerTy    = is_tc integerTyConKey
 isIntTy        = is_tc intTyConKey
 isAddrTy       = is_tc addrTyConKey
@@ -645,24 +743,6 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 %************************************************************************
 
 \begin{code}
-hoistForAllTys :: Type -> Type
-       -- Move all the foralls to the top
-       -- e.g.  T -> forall a. a  ==>   forall a. T -> a
-        -- Careful: LOSES USAGE ANNOTATIONS!
-hoistForAllTys ty
-  = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
-  where
-    hoist :: Type -> ([TyVar], Type)
-    hoist ty = case tcSplitFunTys    ty  of { (args, res) -> 
-              case tcSplitForAllTys res of {
-                 ([], body)  -> ([], ty) ;
-                 (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
-                                  (tvs1 ++ tvs2, mkFunTys args body2)
-              }}}
-\end{code}
-
-
-\begin{code}
 deNoteType :: Type -> Type
        -- Remove synonyms, but not source types
 deNoteType ty@(TyVarTy tyvar)  = ty
@@ -672,43 +752,45 @@ deNoteType (NoteTy _ ty)  = deNoteType ty
 deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
 deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
 deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)
-deNoteType (UsageTy u ty)      = UsageTy u (deNoteType ty)
 
 deNoteSourceType :: SourceType -> SourceType
-deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
-deNoteSourceType (IParam n ty)  = IParam n (deNoteType ty)
-deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
+deNoteSourceType (ClassP c tys)   = ClassP c (map deNoteType tys)
+deNoteSourceType (IParam n ty)    = IParam n (deNoteType ty)
+deNoteSourceType (NType tc tys)   = NType tc (map deNoteType tys)
 \end{code}
 
-Find the free names of a type, including the type constructors and classes it mentions
-This is used in the front end of the compiler
+Find the free tycons and classes of a type.  This is used in the front
+end of the compiler.
 
 \begin{code}
-namesOfType :: Type -> NameSet
-namesOfType (TyVarTy tv)               = unitNameSet (getName tv)
-namesOfType (TyConApp tycon tys)       = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
-namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
-namesOfType (NoteTy other_note    ty2) = namesOfType ty2
-namesOfType (SourceTy (IParam n ty))   = namesOfType ty
-namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
-namesOfType (SourceTy (NType tc tys))  = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
-namesOfType (FunTy arg res)            = namesOfType arg `unionNameSets` namesOfType res
-namesOfType (AppTy fun arg)            = namesOfType fun `unionNameSets` namesOfType arg
-namesOfType (ForAllTy tyvar ty)                = namesOfType ty `delFromNameSet` getName tyvar
-namesOfType (UsageTy u ty)             = namesOfType u `unionNameSets` namesOfType ty
-
-namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
-
-namesOfDFunHead :: Type -> NameSet
+tyClsNamesOfType :: Type -> NameSet
+tyClsNamesOfType (TyVarTy tv)              = emptyNameSet
+tyClsNamesOfType (TyConApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
+tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (SourceTy (IParam n ty))   = tyClsNamesOfType ty
+tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (SourceTy (NType tc tys))  = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (FunTy arg res)           = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
+tyClsNamesOfType (AppTy fun arg)           = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
+tyClsNamesOfType (ForAllTy tyvar ty)       = tyClsNamesOfType ty
+
+tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
+
+tyClsNamesOfDFunHead :: Type -> NameSet
 -- Find the free type constructors and classes 
 -- of the head of the dfun instance type
 -- The 'dfun_head_type' is because of
 --     instance Foo a => Baz T where ...
 -- The decl is an orphan if Baz and T are both not locally defined,
 --     even if Foo *is* locally defined
-namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
-                               (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
-                                                                     (map getName tvs)
+tyClsNamesOfDFunHead dfun_ty 
+  = case tcSplitSigmaTy dfun_ty of
+       (tvs,_,head_ty) -> tyClsNamesOfType head_ty
+
+classNamesOfTheta :: ThetaType -> [Name]
+-- Looks just for ClassP things; maybe it should check
+classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
 \end{code}
 
 
@@ -742,26 +824,87 @@ isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 isFFIDynArgumentTy :: Type -> Bool
 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 
 isFFIDynResultTy :: Type -> Bool
 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
 
 isFFILabelTy :: Type -> Bool
 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 -- or a newtype of either.
-isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
+isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey]
+
+isFFIDotnetTy :: DynFlags -> Type -> Bool
+isFFIDotnetTy dflags ty
+  = checkRepTyCon (\ tc -> not (isByteArrayLikeTyCon tc) &&
+                          (legalFIResultTyCon dflags tc || 
+                          isFFIDotnetObjTy ty || isStringTy ty)) ty
+
+-- Support String as an argument or result from a .NET FFI call.
+isStringTy ty = 
+  case tcSplitTyConApp_maybe (repType ty) of
+    Just (tc, [arg_ty])
+      | tc == listTyCon ->
+        case tcSplitTyConApp_maybe (repType arg_ty) of
+         Just (cc,[]) -> cc == charTyCon
+         _ -> False
+    _ -> False
+
+-- Support String as an argument or result from a .NET FFI call.
+isFFIDotnetObjTy ty = 
+  let
+   (_, t_ty) = tcSplitForAllTys ty
+  in
+  case tcSplitTyConApp_maybe (repType t_ty) of
+    Just (tc, [arg_ty]) | getName tc == objectTyConName -> True
+    _ -> False
+
+toDNType :: Type -> DNType
+toDNType ty
+  | isStringTy ty = DNString
+  | isFFIDotnetObjTy ty = DNObject
+  | Just (tc,argTys) <- tcSplitTyConApp_maybe ty = 
+     case lookup (getUnique tc) dn_assoc of
+       Just x  -> x
+       Nothing 
+         | tc `hasKey` ioTyConKey -> toDNType (head argTys)
+        | otherwise -> pprPanic ("toDNType: unsupported .NET type") (pprType ty <+> parens (hcat (map pprType argTys)) <+> ppr tc)
+    where
+      dn_assoc :: [ (Unique, DNType) ]
+      dn_assoc = [ (unitTyConKey,   DNUnit)
+                , (intTyConKey,    DNInt)
+                , (int8TyConKey,   DNInt8)
+                , (int16TyConKey,  DNInt16)
+                , (int32TyConKey,  DNInt32)
+                , (int64TyConKey,  DNInt64)
+                , (wordTyConKey,   DNInt)
+                , (word8TyConKey,  DNWord8)
+                , (word16TyConKey, DNWord16)
+                , (word32TyConKey, DNWord32)
+                , (word64TyConKey, DNWord64)
+                , (floatTyConKey,  DNFloat)
+                , (doubleTyConKey, DNDouble)
+                , (addrTyConKey,   DNPtr)
+                , (ptrTyConKey,    DNPtr)
+                , (funPtrTyConKey, DNPtr)
+                , (charTyConKey,   DNChar)
+                , (boolTyConKey,   DNBool)
+                ]
 
 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
        -- Look through newtypes
        -- Non-recursive ones are transparent to splitTyConApp,
-       -- but recursive ones aren't; hence the splitNewType_maybe
+       -- but recursive ones aren't
 checkRepTyCon check_tc ty 
-  | Just ty'    <- splitNewType_maybe ty  = checkRepTyCon check_tc ty'
-  | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
-  | otherwise                            = False
+  | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
+  | otherwise                                      = False
+
+checkRepTyConKey :: [Unique] -> Type -> Bool
+-- Like checkRepTyCon, but just looks at the TyCon key
+checkRepTyConKey keys
+  = checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
 \end{code}
 
 ----------------------------------------------
@@ -774,8 +917,7 @@ legalFEArgTyCon :: TyCon -> Bool
 -- bytearrays from a _ccall_ / foreign declaration
 -- (or be passed them as arguments in foreign exported functions).
 legalFEArgTyCon tc
-  | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
-                         byteArrayTyConKey, mutableByteArrayTyConKey ] 
+  | isByteArrayLikeTyCon tc
   = False
   -- It's also illegal to make foreign exports that take unboxed
   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
@@ -784,24 +926,20 @@ legalFEArgTyCon tc
 
 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 legalFIResultTyCon dflags tc
-  | getUnique tc `elem`
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
-  | tc == unitTyCon = True
-  | otherwise      = marshalableTyCon dflags tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise              = marshalableTyCon dflags tc
 
 legalFEResultTyCon :: TyCon -> Bool
 legalFEResultTyCon tc
-  | getUnique tc `elem` 
-       [ foreignObjTyConKey, foreignPtrTyConKey,
-         byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
-  | tc == unitTyCon = True
-  | otherwise       = boxedMarshalableTyCon tc
+  | isByteArrayLikeTyCon tc = False
+  | tc == unitTyCon         = True
+  | otherwise               = boxedMarshalableTyCon tc
 
 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 -- Checks validity of types going from Haskell -> external world
 legalOutgoingTyCon dflags safety tc
-  | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+  | playSafe safety && isByteArrayLikeTyCon tc
   = False
   | otherwise
   = marshalableTyCon dflags tc
@@ -817,45 +955,16 @@ boxedMarshalableTyCon tc
                         , word32TyConKey, word64TyConKey
                         , floatTyConKey, doubleTyConKey
                         , addrTyConKey, ptrTyConKey, funPtrTyConKey
-                        , charTyConKey, foreignObjTyConKey
-                        , foreignPtrTyConKey
+                        , charTyConKey
                         , stablePtrTyConKey
                         , byteArrayTyConKey, mutableByteArrayTyConKey
                         , boolTyConKey
                         ]
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
-(allDistinctTyVars tys tvs) = True 
-       iff 
-all the types tys are type variables, 
-distinct from each other and from tvs.
-
-This is useful when checking that unification hasn't unified signature
-type variables.  For example, if the type sig is
-       f :: forall a b. a -> b -> b
-we want to check that 'a' and 'b' havn't 
-       (a) been unified with a non-tyvar type
-       (b) been unified with each other (all distinct)
-       (c) been unified with a variable free in the environment
-
-\begin{code}
-allDistinctTyVars :: [Type] -> TyVarSet -> Bool
 
-allDistinctTyVars []       acc
-  = True
-allDistinctTyVars (ty:tys) acc 
-  = case tcGetTyVar_maybe ty of
-       Nothing                       -> False  -- (a)
-       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
-               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
-\end{code}    
+isByteArrayLikeTyCon :: TyCon -> Bool
+isByteArrayLikeTyCon tc = 
+  getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
+\end{code}
 
 
 %************************************************************************
@@ -950,10 +1059,6 @@ uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 #endif
 
-       -- Ignore usages
-uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
-uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
-
        -- Anything else fails
 uTysX ty1 ty2 k subst = Nothing
 
@@ -974,7 +1079,6 @@ uVarX tv1 ty2 k subst@(tmpls, env)
               |  typeKind ty2 `eqKind` tyVarKind tv1
               && occur_check_ok ty2
               ->     -- No kind mismatch nor occur check
-                 UASSERT( not (isUTy ty2) )
                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 
               | otherwise -> Nothing   -- Fail if kind mis-match or occur check
@@ -1042,8 +1146,15 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-       Nothing -> UASSERT( not (isUTy ty) )
-                   k (extendSubstEnv senv v (DoneTy ty))
+       Nothing | typeKind ty `eqKind` tyVarKind v      
+                       -- We do a kind check, just as in the uVarX above
+                       -- The kind check is needed to avoid bogus matches
+                       -- of   (a b) with (c d), where the kinds don't match
+                       -- An occur check isn't needed when matching.
+               -> k (extendSubstEnv senv v (DoneTy ty))
+
+               | otherwise  -> Nothing -- Fails
+
        Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
                           | otherwise           -> Nothing  -- Fails
 
@@ -1084,9 +1195,6 @@ match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 
-match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-
        -- With type synonyms, we have to be careful for the exact
        -- same reasons as in the unifier.  Please see the
        -- considerable commentary there before changing anything