Improve crash message from applyTys and applyTypeToArgs

[ghc-hetmet.git] / compiler / types / FamInstEnv.lhs

diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index b9276b7..ba96a55 100644 (file)
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -10,28 +10,32 @@ module FamInstEnv (
        pprFamInst, pprFamInstHdr, pprFamInsts, 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 
        pprFamInst, pprFamInstHdr, pprFamInsts, 
        famInstHead, mkLocalFamInst, mkImportedFamInst,
 

-       FamInstEnvs, FamInstEnv, emptyFamInstEnv, 
+       FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 

        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 
        extendFamInstEnv, extendFamInstEnvList, 
        famInstEnvElts, familyInstances,
 

-       lookupFamInstEnv, lookupFamInstEnvUnify
+       lookupFamInstEnv, lookupFamInstEnvUnify,
+       
+       -- Normalisation
+       topNormaliseType

     ) where
 
 #include "HsVersions.h"
 
 import InstEnv
 import Unify
     ) where
 
 #include "HsVersions.h"
 
 import InstEnv
 import Unify

-import TcGadt
-import TcType

 import Type
 import Type

+import TypeRep

 import TyCon
 import TyCon

+import Coercion

 import VarSet
 import Var
 import Name
 import VarSet
 import Var
 import Name

-import OccName
-import SrcLoc

 import UniqFM
 import Outputable
 import UniqFM
 import Outputable

+import Maybes
+import Util
+import FastString

 
 import Maybe
 \end{code}
 
 import Maybe
 \end{code}

@@ -46,13 +50,19 @@ import Maybe
 \begin{code}
 data FamInst 
   = FamInst { fi_fam   :: Name         -- Family name
 \begin{code}
 data FamInst 
   = FamInst { fi_fam   :: Name         -- Family name

+               -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
+               --                         Just (tc, tys) -> tc

 
                -- Used for "rough matching"; same idea as for class instances
            , fi_tcs   :: [Maybe Name]  -- Top of type args
 
                -- Used for "rough matching"; same idea as for class instances
            , fi_tcs   :: [Maybe Name]  -- Top of type args

+               -- INVARIANT: fi_tcs = roughMatchTcs fi_tys

 
                -- Used for "proper matching"; ditto
            , fi_tvs   :: TyVarSet      -- Template tyvars for full match
            , fi_tys   :: [Type]        -- Full arg types
 
                -- Used for "proper matching"; ditto
            , fi_tvs   :: TyVarSet      -- Template tyvars for full match
            , fi_tys   :: [Type]        -- Full arg types

+               -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
+               --            fi_tys = case tyConFamInst_maybe fi_tycon of
+               --                         Just (_, tys) -> tys

 
            , fi_tycon :: TyCon         -- Representation tycon
            }
 
            , fi_tycon :: TyCon         -- Representation tycon
            }

@@ -62,6 +72,7 @@ data FamInst
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
 
 famInstTyCon :: FamInst -> TyCon
 famInstTyCon = fi_tycon
 

+famInstTyVars :: FamInst -> TyVarSet

 famInstTyVars = fi_tvs
 \end{code}
 
 famInstTyVars = fi_tvs
 \end{code}
 

@@ -76,17 +87,16 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)

-       2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc famInst)))
+       2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))

 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
   = pprTyConSort <+> pprHead
   where

-    pprHead = parenSymOcc (getOccName fam) (ppr fam) <+> 
-             sep (map pprParendType tys)
-    pprTyConSort | isDataTyCon tycon = ptext SLIT("data instance")
-                | isNewTyCon  tycon = ptext SLIT("newtype instance")
-                | isSynTyCon  tycon = ptext SLIT("type instance")
+    pprHead = pprTypeApp fam tys
+    pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
+                | isNewTyCon  tycon = ptext (sLit "newtype instance")
+                | isSynTyCon  tycon = ptext (sLit "type instance")

                 | otherwise         = panic "FamInstEnv.pprFamInstHdr"
 
 pprFamInsts :: [FamInst] -> SDoc
                 | otherwise         = panic "FamInstEnv.pprFamInstHdr"
 
 pprFamInsts :: [FamInst] -> SDoc

@@ -156,6 +166,9 @@ data FamilyInstEnv
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
 
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
 

+emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
+emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
+

 emptyFamInstEnv :: FamInstEnv
 emptyFamInstEnv = emptyUFM
 
 emptyFamInstEnv :: FamInstEnv
 emptyFamInstEnv = emptyUFM
 

@@ -184,7 +197,7 @@ extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

-\subsection{Looking up a family instance}
+               Looking up a family instance

 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

@@ -193,11 +206,28 @@ Multiple matches are only possible in case of type families (not data
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 
 families), and then, it doesn't matter which match we choose (as the
 instances are guaranteed confluent).
 

+We return the matching family instances and the type instance at which it
+matches.  For example, if we lookup 'T [Int]' and have a family instance
+
+  data instance T [a] = ..
+
+desugared to
+
+  data :R42T a = ..
+  coe :Co:R42T a :: T [a] ~ :R42T a
+
+we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
+

 \begin{code}
 \begin{code}

+type FamInstMatch = (FamInst, [Type])           -- Matching type instance
+

 lookupFamInstEnv :: FamInstEnvs
                 -> TyCon -> [Type]             -- What we are looking for
 lookupFamInstEnv :: FamInstEnvs
                 -> TyCon -> [Type]             -- What we are looking for

-                -> [(TvSubst, FamInst)]        -- Successful matches
+                -> [FamInstMatch]              -- Successful matches

 lookupFamInstEnv (pkg_ie, home_ie) fam tys
 lookupFamInstEnv (pkg_ie, home_ie) fam tys

+  | not (isOpenTyCon fam) 
+  = []
+  | otherwise

   = home_matches ++ pkg_matches
   where
     rough_tcs    = roughMatchTcs tys
   = home_matches ++ pkg_matches
   where
     rough_tcs    = roughMatchTcs tys

@@ -226,7 +256,7 @@ lookupFamInstEnv (pkg_ie, home_ie) fam tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
 
         -- Proper check
       | Just subst <- tcMatchTys tpl_tvs tpl_tys tys

-      = (subst, item) : find rest
+      = (item, substTyVars subst (tyConTyVars tycon)) : find rest

 
         -- No match => try next
       | otherwise
 
         -- No match => try next
       | otherwise

@@ -245,8 +275,11 @@ indexed synonyms and we don't want to slow that down by needless unification.
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
 
 \begin{code}
 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]

-                     -> [(TvSubst, FamInst)]
+                     -> [(FamInstMatch, TvSubst)]

 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys

+  | not (isOpenTyCon fam) 
+  = []
+  | otherwise

   = home_matches ++ pkg_matches
   where
     rough_tcs    = roughMatchTcs tys
   = home_matches ++ pkg_matches
   where
     rough_tcs    = roughMatchTcs tys

@@ -280,12 +313,129 @@ lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
                )
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them
                )
                -- Unification will break badly if the variables overlap
                -- They shouldn't because we allocate separate uniques for them

-        case tcUnifyTys bind_fn tpl_tys tys of
-           Just subst -> (subst, item) : find rest
+        case tcUnifyTys instanceBindFun tpl_tys tys of
+           Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
+                          in
+                          ((item, rep_tys), subst) : find rest

            Nothing    -> find rest
            Nothing    -> find rest

+\end{code}

 
 

--- See explanation at @InstEnv.bind_fn@.
---
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
-          | otherwise                             = BindMe
+%************************************************************************
+%*                                                                     *
+               Looking up a family instance
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+topNormaliseType :: FamInstEnvs
+                -> Type
+                -> Maybe (Coercion, Type)
+
+-- Get rid of *outermost* (or toplevel) 
+--     * type functions 
+--     * newtypes
+-- using appropriate coercions.
+-- By "outer" we mean that toplevelNormaliseType guarantees to return
+-- a type that does not have a reducible redex (F ty1 .. tyn) as its
+-- outermost form.  It *can* return something like (Maybe (F ty)), where
+-- (F ty) is a redex.
+
+-- Its a bit like Type.repType, but handles type families too
+
+topNormaliseType env ty
+  = go [] ty
+  where
+    go :: [TyCon] -> Type -> Maybe (Coercion, Type)
+    go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
+       = go rec_nts ty'        
+
+    go rec_nts (TyConApp tc tys)               -- Expand newtypes
+       | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
+       = if tc `elem` rec_nts                  --  in Type.lhs
+         then Nothing
+         else let nt_co = mkTyConApp co_con tys
+              in add_co nt_co rec_nts' nt_rhs
+       where
+         nt_rhs = newTyConInstRhs tc tys
+         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                  | otherwise           = rec_nts
+
+    go rec_nts (TyConApp tc tys)               -- Expand open tycons
+       | isOpenTyCon tc
+       , (ACo co, ty) <- normaliseTcApp env tc tys
+       =       -- The ACo says "something happened"
+               -- Note that normaliseType fully normalises, but it has do to so
+               -- to be sure that 
+          add_co co rec_nts ty
+
+    go _ _ = Nothing
+
+    add_co co rec_nts ty 
+       = case go rec_nts ty of
+               Nothing         -> Just (co, ty)
+               Just (co', ty') -> Just (mkTransCoercion co co', ty')
+        
+
+---------------
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
+normaliseTcApp env tc tys
+  = let        -- First normalise the arg types so that they'll match 
+       -- when we lookup in in the instance envt
+       (cois, ntys) = mapAndUnzip (normaliseType env) tys
+       tycon_coi    = mkTyConAppCoI tc ntys cois
+    in         -- Now try the top-level redex
+    case lookupFamInstEnv env tc ntys of
+               -- A matching family instance exists
+       [(fam_inst, tys)] -> (fix_coi, nty)
+           where
+               rep_tc         = famInstTyCon fam_inst
+               co_tycon       = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+               co             = mkTyConApp co_tycon tys
+               first_coi      = mkTransCoI tycon_coi (ACo co)
+               (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
+               fix_coi        = mkTransCoI first_coi rest_coi
+
+               -- No unique matching family instance exists;
+               -- we do not do anything
+       _ -> (tycon_coi, TyConApp tc ntys)
+---------------
+normaliseType :: FamInstEnvs           -- environment with family instances
+             -> Type                   -- old type
+             -> (CoercionI, Type)      -- (coercion,new type), where
+                                       -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating *all* type-function redexes
+-- Returns with IdCo if nothing happens
+
+normaliseType env ty 
+  | Just ty' <- coreView ty = normaliseType env ty' 
+normaliseType env (TyConApp tc tys)
+  = normaliseTcApp env tc tys
+normaliseType env (AppTy ty1 ty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+normaliseType env (FunTy ty1 ty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+normaliseType env (ForAllTy tyvar ty1)
+  = let (coi,nty1) = normaliseType env ty1
+    in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+normaliseType _   ty@(TyVarTy _)
+  = (IdCo,ty)
+normaliseType env (PredTy predty)
+  = normalisePred env predty
+
+---------------
+normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normalisePred env (ClassP cls tys)
+  =    let (cois,tys') = mapAndUnzip (normaliseType env) tys
+       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+normalisePred env (IParam ipn ty)
+  =    let (coi,ty') = normaliseType env ty
+       in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+normalisePred env (EqPred ty1 ty2)
+  =    let (coi1,ty1') = normaliseType env ty1
+            (coi2,ty2') = normaliseType env ty2
+       in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')

 \end{code}
 \end{code}