FamInstEnv.lhs 14.4 KB
Newer Older
1 2 3 4 5
%
% (c) The University of Glasgow 2006
%

FamInstEnv: Type checked family instance declarations
6 7 8

\begin{code}
module FamInstEnv (
9 10
	FamInst(..), famInstTyCon, famInstTyVars, 
	pprFamInst, pprFamInstHdr, pprFamInsts, 
11
	famInstHead, mkLocalFamInst, mkImportedFamInst,
12

13
	FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 
14
	extendFamInstEnv, extendFamInstEnvList, 
15
	famInstEnvElts, familyInstances,
16

TomSchrijvers's avatar
TomSchrijvers committed
17 18 19
	lookupFamInstEnv, lookupFamInstEnvUnify,
	
	-- Normalisation
20
	topNormaliseType
21 22 23 24
    ) where

#include "HsVersions.h"

25 26
import InstEnv
import TcType
27
import Unify
28
import Type
TomSchrijvers's avatar
TomSchrijvers committed
29
import TypeRep
30
import TyCon
TomSchrijvers's avatar
TomSchrijvers committed
31
import Coercion
32 33 34 35
import VarSet
import Var
import Name
import UniqFM
36
import Outputable
TomSchrijvers's avatar
TomSchrijvers committed
37 38
import Maybes
import Util
39
import FastString
40

41
import Maybe
42 43 44 45 46 47 48 49 50 51 52 53
\end{code}


%************************************************************************
%*									*
\subsection{Type checked family instance heads}
%*									*
%************************************************************************

\begin{code}
data FamInst 
  = FamInst { fi_fam   :: Name		-- Family name
54 55
		-- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
		--			   Just (tc, tys) -> tc
56 57 58

		-- Used for "rough matching"; same idea as for class instances
	    , fi_tcs   :: [Maybe Name]	-- Top of type args
59
		-- INVARIANT: fi_tcs = roughMatchTcs fi_tys
60 61

		-- Used for "proper matching"; ditto
62 63
	    , fi_tvs   :: TyVarSet	-- Template tyvars for full match
	    , fi_tys   :: [Type]	-- Full arg types
64 65 66
		-- INVARIANT: fi_tvs = tyConTyVars fi_tycon
		--	      fi_tys = case tyConFamInst_maybe fi_tycon of
		--			   Just (_, tys) -> tys
67 68 69 70 71 72 73 74

	    , fi_tycon :: TyCon		-- Representation tycon
	    }

-- Obtain the representation tycon of a family instance.
--
famInstTyCon :: FamInst -> TyCon
famInstTyCon = fi_tycon
75

twanvl's avatar
twanvl committed
76
famInstTyVars :: FamInst -> TyVarSet
77
famInstTyVars = fi_tvs
78 79 80 81 82 83 84 85 86 87 88 89 90
\end{code}

\begin{code}
instance NamedThing FamInst where
   getName = getName . fi_tycon

instance Outputable FamInst where
   ppr = pprFamInst

-- Prints the FamInst as a family instance declaration
pprFamInst :: FamInst -> SDoc
pprFamInst famInst
  = hang (pprFamInstHdr famInst)
Ian Lynagh's avatar
Ian Lynagh committed
91
	2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
92 93 94 95 96

pprFamInstHdr :: FamInst -> SDoc
pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
  = pprTyConSort <+> pprHead
  where
97
    pprHead = pprTypeApp fam tys
Ian Lynagh's avatar
Ian Lynagh committed
98 99 100
    pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
		 | isNewTyCon  tycon = ptext (sLit "newtype instance")
		 | isSynTyCon  tycon = ptext (sLit "type instance")
101 102 103 104
		 | otherwise	     = panic "FamInstEnv.pprFamInstHdr"

pprFamInsts :: [FamInst] -> SDoc
pprFamInsts finsts = vcat (map pprFamInst finsts)
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142

famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
famInstHead (FamInst {fi_tycon = tycon})
  = case tyConFamInst_maybe tycon of
      Nothing         -> panic "FamInstEnv.famInstHead"
      Just (fam, tys) -> (tyConTyVars tycon, fam, tys)

-- Make a family instance representation from a tycon.  This is used for local
-- instances, where we can safely pull on the tycon.
--
mkLocalFamInst :: TyCon -> FamInst
mkLocalFamInst tycon
  = case tyConFamInst_maybe tycon of
           Nothing         -> panic "FamInstEnv.mkLocalFamInst"
	   Just (fam, tys) -> 
	     FamInst {
	       fi_fam   = tyConName fam,
	       fi_tcs   = roughMatchTcs tys,
	       fi_tvs   = mkVarSet . tyConTyVars $ tycon,
	       fi_tys   = tys,
	       fi_tycon = tycon
	     }

-- Make a family instance representation from the information found in an
-- unterface file.  In particular, we get the rough match info from the iface
-- (instead of computing it here).
--
mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
mkImportedFamInst fam mb_tcs tycon
  = FamInst {
      fi_fam   = fam,
      fi_tcs   = mb_tcs,
      fi_tvs   = mkVarSet . tyConTyVars $ tycon,
      fi_tys   = case tyConFamInst_maybe tycon of
		   Nothing       -> panic "FamInstEnv.mkImportedFamInst"
		   Just (_, tys) -> tys,
      fi_tycon = tycon
    }
143 144 145 146 147 148 149 150 151 152 153 154
\end{code}


%************************************************************************
%*									*
		FamInstEnv
%*									*
%************************************************************************

InstEnv maps a family name to the list of known instances for that family.

\begin{code}
155 156
type FamInstEnv = UniqFM FamilyInstEnv	-- Maps a family to its instances

157 158 159
type FamInstEnvs = (FamInstEnv, FamInstEnv)
 	-- External package inst-env, Home-package inst-env

160 161 162 163 164
data FamilyInstEnv
  = FamIE [FamInst]	-- The instances for a particular family, in any order
  	  Bool 		-- True <=> there is an instance of form T a b c
			-- 	If *not* then the common case of looking up
			--	(T a b c) can fail immediately
165 166 167 168 169

-- INVARIANTS:
--  * The fs_tvs are distinct in each FamInst
--	of a range value of the map (so we can safely unify them)

170 171 172
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)

173 174 175 176
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnv = emptyUFM

famInstEnvElts :: FamInstEnv -> [FamInst]
177
famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
178 179 180 181 182 183

familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyInstances (pkg_fie, home_fie) fam
  = get home_fie ++ get pkg_fie
  where
    get env = case lookupUFM env fam of
184 185
		Just (FamIE insts _) -> insts
		Nothing	             -> []
186 187 188 189 190

extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis

extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
191 192
extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
  = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
193
  where
194 195 196
    add (FamIE items tyvar) _ = FamIE (ins_item:items)
				      (ins_tyvar || tyvar)
    ins_tyvar = not (any isJust mb_tcs)
197
\end{code}
198

199 200
%************************************************************************
%*									*
201
		Looking up a family instance
202 203 204 205 206 207 208 209
%*									*
%************************************************************************

@lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
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).

210 211 212 213 214 215 216 217 218 219 220 221
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)'.

222
\begin{code}
223 224
type FamInstMatch = (FamInst, [Type])           -- Matching type instance

225
lookupFamInstEnv :: FamInstEnvs
226
	         -> TyCon -> [Type]		-- What we are looking for
227
	         -> [FamInstMatch] 	        -- Successful matches
228
lookupFamInstEnv (pkg_ie, home_ie) fam tys
229 230 231
  | not (isOpenTyCon fam) 
  = []
  | otherwise
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
  = home_matches ++ pkg_matches
  where
    rough_tcs    = roughMatchTcs tys
    all_tvs      = all isNothing rough_tcs
    home_matches = lookup home_ie 
    pkg_matches  = lookup pkg_ie  

    --------------
    lookup env = case lookupUFM env fam of
		   Nothing -> []	-- No instances for this class
		   Just (FamIE insts has_tv_insts)
		       -- Short cut for common case:
		       --   The thing we are looking up is of form (C a
		       --   b c), and the FamIE has no instances of
		       --   that form, so don't bother to search 
		     | all_tvs && not has_tv_insts -> []
		     | otherwise                   -> find insts

    --------------
251
    find [] = []
252 253 254 255 256 257 258 259
    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
			  fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
	-- Fast check for no match, uses the "rough match" fields
      | instanceCantMatch rough_tcs mb_tcs
      = find rest

        -- Proper check
      | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
260
      = (item, substTyVars subst (tyConTyVars tycon)) : find rest
261 262 263 264 265

        -- No match => try next
      | otherwise
      = find rest
\end{code}
266 267 268 269 270 271 272 273 274 275 276 277 278

While @lookupFamInstEnv@ uses a one-way match, the next function
@lookupFamInstEnvUnify@ uses two-way matching (ie, unification).  This is
needed to check for overlapping instances.

For class instances, these two variants of lookup are combined into one
function (cf, @InstEnv@).  We don't do that for family instances as the
results of matching and unification are used in two different contexts.
Moreover, matching is the wildly more frequently used operation in the case of
indexed synonyms and we don't want to slow that down by needless unification.

\begin{code}
lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
279
	              -> [(FamInstMatch, TvSubst)]
280
lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
281 282 283
  | not (isOpenTyCon fam) 
  = []
  | otherwise
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
  = home_matches ++ pkg_matches
  where
    rough_tcs    = roughMatchTcs tys
    all_tvs      = all isNothing rough_tcs
    home_matches = lookup home_ie 
    pkg_matches  = lookup pkg_ie  

    --------------
    lookup env = case lookupUFM env fam of
		   Nothing -> []	-- No instances for this class
		   Just (FamIE insts has_tv_insts)
		       -- Short cut for common case:
		       --   The thing we are looking up is of form (C a
		       --   b c), and the FamIE has no instances of
		       --   that form, so don't bother to search 
		     | all_tvs && not has_tv_insts -> []
		     | otherwise                   -> find insts

    --------------
    find [] = []
    find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
			  fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
	-- Fast check for no match, uses the "rough match" fields
      | instanceCantMatch rough_tcs mb_tcs
      = find rest

      | otherwise
      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
		 (ppr fam <+> ppr tys <+> ppr all_tvs) $$
		 (ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
		)
		-- 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
318 319
	    Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
                          in
320
                          ((item, rep_tys), subst) : find rest
321 322 323 324
	    Nothing    -> find rest

-- See explanation at @InstEnv.bind_fn@.
--
twanvl's avatar
twanvl committed
325
bind_fn :: TyVar -> BindFlag
326 327 328
bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
	   | otherwise	 		 	   = BindMe
\end{code}
TomSchrijvers's avatar
TomSchrijvers committed
329

330 331 332 333 334
%************************************************************************
%*									*
		Looking up a family instance
%*									*
%************************************************************************
TomSchrijvers's avatar
TomSchrijvers committed
335 336

\begin{code}
337
topNormaliseType :: FamInstEnvs
338 339
		 -> Type
	   	 -> Maybe (Coercion, Type)
340

341 342 343 344
-- Get rid of *outermost* (or toplevel) 
--	* type functions 
--	* newtypes
-- using appropriate coercions.
345 346 347 348 349
-- 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.

350
-- Its a bit like Type.repType, but handles type families too
351 352

topNormaliseType env ty
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
  = 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

twanvl's avatar
twanvl committed
378
    go _ _ = Nothing
379 380 381 382 383

    add_co co rec_nts ty 
	= case go rec_nts ty of
		Nothing 	-> Just (co, ty)
		Just (co', ty') -> Just (mkTransCoercion co co', ty')
TomSchrijvers's avatar
TomSchrijvers committed
384 385
	 

386 387 388 389 390
---------------
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
391
	(cois, ntys) = mapAndUnzip (normaliseType env) tys
392
	tycon_coi    = mkTyConAppCoI tc ntys cois
393
    in 	-- Now try the top-level redex
394
    case lookupFamInstEnv env tc ntys of
395 396 397 398 399 400 401 402 403 404 405
		-- 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;
TomSchrijvers's avatar
TomSchrijvers committed
406
		-- we do not do anything
twanvl's avatar
twanvl committed
407
	_ -> (tycon_coi, TyConApp tc ntys)
408 409 410 411 412 413 414
---------------
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
415

416 417
normaliseType env ty 
  | Just ty' <- coreView ty = normaliseType env ty' 
twanvl's avatar
twanvl committed
418
normaliseType env (TyConApp tc tys)
419
  = normaliseTcApp env tc tys
twanvl's avatar
twanvl committed
420
normaliseType env (AppTy ty1 ty2)
421 422 423
  = let (coi1,nty1) = normaliseType env ty1
        (coi2,nty2) = normaliseType env ty2
    in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
twanvl's avatar
twanvl committed
424
normaliseType env (FunTy ty1 ty2)
425 426 427
  = let (coi1,nty1) = normaliseType env ty1
        (coi2,nty2) = normaliseType env ty2
    in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
twanvl's avatar
twanvl committed
428
normaliseType env (ForAllTy tyvar ty1)
429 430
  = let (coi,nty1) = normaliseType env ty1
    in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
twanvl's avatar
twanvl committed
431
normaliseType _   ty@(TyVarTy _)
432
  = (IdCo,ty)
433
normaliseType env (PredTy predty)
twanvl's avatar
twanvl committed
434
  = normalisePred env predty
435

436
---------------
437 438 439
normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
normalisePred env (ClassP cls tys)
  =	let (cois,tys') = mapAndUnzip (normaliseType env) tys
TomSchrijvers's avatar
TomSchrijvers committed
440
	in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
441 442
normalisePred env (IParam ipn ty)
  = 	let (coi,ty') = normaliseType env ty
TomSchrijvers's avatar
TomSchrijvers committed
443
	in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
444 445 446
normalisePred env (EqPred ty1 ty2)
  = 	let (coi1,ty1') = normaliseType env ty1
            (coi2,ty2') = normaliseType env ty2
TomSchrijvers's avatar
TomSchrijvers committed
447 448
	in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
\end{code}