Major refactoring of CoAxioms
[ghc.git] / compiler / typecheck / TcInstDcls.lhs
index 11ec175..ac9769c 100644 (file)
@@ -366,40 +366,30 @@ tcInstDecls1    -- Deal with both source-code and imported instance decls
 
 tcInstDecls1 tycl_decls inst_decls deriv_decls 
   = checkNoErrs $
-    do {        -- Stop if addInstInfos etc discovers any errors
-                -- (they recover, so that we get more than one error each
-                -- round)
-
-                -- (1) Do class and family instance declarations
-       ; idx_tycons        <- mapAndRecoverM tcTopFamInstDecl $
-                              filter (isFamInstDecl . unLoc) tycl_decls
-       ; local_info_tycons <- mapAndRecoverM tcLocalInstDecl1  inst_decls
-
-       ; let { (local_info,
-                at_tycons_s)   = unzip local_info_tycons
-             ; at_idx_tycons   = concat at_tycons_s ++ idx_tycons
-             ; at_things       = map ATyCon at_idx_tycons }
-
-                -- (2) Add the tycons of indexed types and their implicit
-                --     tythings to the global environment
-       ; tcExtendGlobalEnvImplicit at_things $ do
-       { tcg_env <- tcAddImplicits at_things
-       ; setGblEnv tcg_env $
-
-
-                -- Next, construct the instance environment so far, consisting
-                -- of
-                --   (a) local instance decls
-                --   (b) local family instance decls
-         addInsts local_info         $
-         addFamInsts at_idx_tycons   $ do {
-
-                -- (3) Compute instances from "deriving" clauses;
-                -- This stuff computes a context for the derived instance
-                -- decl, so it needs to know about all the instances possible
-                -- NB: class instance declarations can contain derivings as
-                --     part of associated data type declarations
-         failIfErrsM    -- If the addInsts stuff gave any errors, don't
+    do {    -- Stop if addInstInfos etc discovers any errors
+            -- (they recover, so that we get more than one error each
+            -- round)
+
+            -- (1) Do class and family instance declarations
+       ; fam_insts       <- mapAndRecoverM tcTopFamInstDecl $
+                            filter (isFamInstDecl . unLoc) tycl_decls
+       ; inst_decl_stuff <- mapAndRecoverM tcLocalInstDecl1  inst_decls
+
+       ; let { (local_info, at_fam_insts_s) = unzip inst_decl_stuff
+             ; all_fam_insts = concat at_fam_insts_s ++ fam_insts }
+
+            -- (2) Next, construct the instance environment so far, consisting of
+            --   (a) local instance decls
+            --   (b) local family instance decls
+       ; addClsInsts local_info      $
+         addFamInsts all_fam_insts   $ do
+
+            -- (3) Compute instances from "deriving" clauses;
+            -- This stuff computes a context for the derived instance
+            -- decl, so it needs to know about all the instances possible
+            -- NB: class instance declarations can contain derivings as
+            --     part of associated data type declarations
+       { failIfErrsM    -- If the addInsts stuff gave any errors, don't
                         -- try the deriving stuff, because that may give
                         -- more errors still
 
@@ -421,24 +411,33 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
        ; return ( gbl_env
                 , (bagToList deriv_inst_info) ++ local_info
                 , deriv_binds)
-    }}}
+    }}
   where
     typInstCheck ty = is_cls (iSpec ty) `elem` typeableClassNames
     typInstErr = ptext $ sLit $ "Can't create hand written instances of Typeable in Safe"
                               ++ " Haskell! Can only derive them"
 
-addInsts :: [InstInfo Name] -> TcM a -> TcM a
-addInsts infos thing_inside
+addClsInsts :: [InstInfo Name] -> TcM a -> TcM a
+addClsInsts infos thing_inside
   = tcExtendLocalInstEnv (map iSpec infos) thing_inside
 
-addFamInsts :: [TyCon] -> TcM a -> TcM a
-addFamInsts tycons thing_inside
-  = tcExtendLocalFamInstEnv (map mkLocalFamInst tycons) thing_inside
+addFamInsts :: [FamInst] -> TcM a -> TcM a
+-- Extend (a) the family instance envt
+--        (b) the type envt with stuff from data type decls
+addFamInsts fam_insts thing_inside
+  = tcExtendLocalFamInstEnv fam_insts $ 
+    tcExtendGlobalEnvImplicit things  $ 
+    do { tcg_env <- tcAddImplicits things
+       ; setGblEnv tcg_env thing_inside }
+  where
+    axioms = map famInstAxiom fam_insts
+    tycons = famInstsRepTyCons fam_insts
+    things = map ATyCon tycons ++ map ACoAxiom axioms 
 \end{code}
 
 \begin{code}
 tcLocalInstDecl1 :: LInstDecl Name
-                 -> TcM (InstInfo Name, [TyCon])
+                 -> TcM (InstInfo Name, [FamInst])
         -- A source-file instance declaration
         -- Type-check all the stuff before the "where"
         --
@@ -457,14 +456,14 @@ tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
                            
         -- Next, process any associated types.
         ; traceTc "tcLocalInstDecl" (ppr poly_ty)
-        ; idx_tycons0 <- tcExtendTyVarEnv tyvars $
-                         mapAndRecoverM (tcAssocDecl clas mini_env) ats
+        ; fam_insts0 <- tcExtendTyVarEnv tyvars $
+                        mapAndRecoverM (tcAssocDecl clas mini_env) ats
 
         -- Check for missing associated types and build them
         -- from their defaults (if available)
         ; let defined_ats = mkNameSet $ map (tcdName . unLoc) ats
 
-              mk_deflt_at_instances :: ClassATItem -> TcM [TyCon]
+              mk_deflt_at_instances :: ClassATItem -> TcM [FamInst]
               mk_deflt_at_instances (fam_tc, defs)
                  -- User supplied instances ==> everything is OK
                 | tyConName fam_tc `elemNameSet` defined_ats 
@@ -487,12 +486,9 @@ tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
                            tvs'     = varSetElems tv_set'
                      ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
                      ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
-                       buildSynTyCon rep_tc_name tvs'
-                                     (SynonymTyCon rhs')
-                                     (typeKind rhs')
-                                     NoParentTyCon (Just (fam_tc, pat_tys')) }
+                       return (mkSynFamInst rep_tc_name tvs' fam_tc pat_tys' rhs') }
 
-        ; idx_tycons1 <- mapM mk_deflt_at_instances (classATItems clas)
+        ; fam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
         
         -- Finally, construct the Core representation of the instance.
         -- (This no longer includes the associated types.)
@@ -504,10 +500,9 @@ tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
               ispec    = mkLocalInstance dfun overlap_flag
               inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }
 
-        ; return (inst_info, idx_tycons0 ++ concat idx_tycons1) }
+        ; return ( inst_info, fam_insts0 ++ concat fam_insts1) }
 \end{code}
 
-
 %************************************************************************
 %*                                                                      *
                Type checking family instances
@@ -520,15 +515,15 @@ lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 
 \begin{code}
-tcTopFamInstDecl :: LTyClDecl Name -> TcM TyCon
+tcTopFamInstDecl :: LTyClDecl Name -> TcM FamInst
 tcTopFamInstDecl (L loc decl)
   = setSrcSpan loc      $
     tcAddDeclCtxt decl  $
     tcFamInstDecl TopLevel decl
 
-tcFamInstDecl :: TopLevelFlag -> TyClDecl Name -> TcM TyCon
+tcFamInstDecl :: TopLevelFlag -> TyClDecl Name -> TcM FamInst
 tcFamInstDecl top_lvl decl
-  = do { -- type family instances require -XTypeFamilies
+  = do { -- Type family instances require -XTypeFamilies
          -- and can't (currently) be in an hs-boot file
        ; traceTc "tcFamInstDecl" (ppr decl)
        ; let fam_tc_lname = tcdLName decl
@@ -546,13 +541,9 @@ tcFamInstDecl top_lvl decl
 
          -- Now check the type/data instance itself
          -- This is where type and data decls are treated separately
-       ; tc <- tcFamInstDecl1 fam_tc decl
-       ; checkValidTyCon tc     -- Remember to check validity;
-                                -- no recursion to worry about here
+       ; tcFamInstDecl1 fam_tc decl }
 
-       ; return tc }
-
-tcFamInstDecl1 :: TyCon -> TyClDecl Name -> TcM TyCon
+tcFamInstDecl1 :: TyCon -> TyClDecl Name -> TcM FamInst
 
   -- "type instance"
 tcFamInstDecl1 fam_tc (decl@TySynonym {})
@@ -563,17 +554,14 @@ tcFamInstDecl1 fam_tc (decl@TySynonym {})
        ; checkValidFamInst t_typats t_rhs
 
          -- (3) construct representation tycon
-       ; rep_tc_name <- newFamInstTyConName (tcdLName decl) t_typats
-       ; buildSynTyCon rep_tc_name t_tvs
-                       (SynonymTyCon t_rhs)
-                       (typeKind t_rhs)
-                       NoParentTyCon (Just (fam_tc, t_typats))
-       }
+       ; rep_tc_name <- newFamInstAxiomName (tcdLName decl) t_typats
+
+       ; return (mkSynFamInst rep_tc_name t_tvs fam_tc t_typats t_rhs) }
 
   -- "newtype instance" and "data instance"
 tcFamInstDecl1 fam_tc (decl@TyData { tcdND = new_or_data, tcdCtxt = ctxt
                                    , tcdTyVars = tvs, tcdTyPats = Just pats
-                                  , tcdCons = cons})
+                                   , tcdCons = cons})
   = do { -- Check that the family declaration is for the right kind
          checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
@@ -595,27 +583,33 @@ tcFamInstDecl1 fam_tc (decl@TyData { tcdND = new_or_data, tcdCtxt = ctxt
 
          -- Construct representation tycon
        ; rep_tc_name <- newFamInstTyConName (tcdLName decl) pats'
+       ; axiom_name  <- newImplicitBinder rep_tc_name mkInstTyCoOcc
        ; let ex_ok = True       -- Existentials ok for type families!
-       ; fixM (\ rep_tycon -> do
-             { let orig_res_ty = mkTyConApp fam_tc pats'
-             ; data_cons <- tcConDecls new_or_data ex_ok rep_tycon
+             orig_res_ty = mkTyConApp fam_tc pats'
+
+       ; (rep_tc, fam_inst) <- fixM $ \ ~(rec_rep_tc, _) ->
+           do { data_cons <- tcConDecls new_or_data ex_ok rec_rep_tc
                                        (tvs', orig_res_ty) cons
-             ; tc_rhs <-
-                 case new_or_data of
-                   DataType -> return (mkDataTyConRhs data_cons)
-                   NewType  -> ASSERT( not (null data_cons) )
-                               mkNewTyConRhs rep_tc_name rep_tycon (head data_cons)
-             ; buildAlgTyCon rep_tc_name tvs' stupid_theta tc_rhs Recursive
-                             h98_syntax NoParentTyCon (Just (fam_tc, pats'))
+              ; tc_rhs <- case new_or_data of
+                     DataType -> return (mkDataTyConRhs data_cons)
+                     NewType  -> ASSERT( not (null data_cons) )
+                                 mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
+              ; let fam_inst = mkDataFamInst axiom_name tvs' fam_tc pats' rep_tc
+                    parent   = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats'
+                    rep_tc   = buildAlgTyCon rep_tc_name tvs' stupid_theta tc_rhs 
+                                             Recursive h98_syntax parent
                  -- We always assume that indexed types are recursive.  Why?
                  -- (1) Due to their open nature, we can never be sure that a
                  -- further instance might not introduce a new recursive
                  -- dependency.  (2) They are always valid loop breakers as
                  -- they involve a coercion.
-             })
-       } }
+              ; return (rep_tc, fam_inst) }
+
+         -- Remember to check validity; no recursion to worry about here
+       ; checkValidTyCon rep_tc
+       ; return fam_inst } }
     where
-         h98_syntax = case cons of      -- All constructors have same shape
+       h98_syntax = case cons of      -- All constructors have same shape
                         L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
                         _ -> True
 
@@ -626,26 +620,28 @@ tcFamInstDecl1 _ d = pprPanic "tcFamInstDecl1" (ppr d)
 tcAssocDecl :: Class           -- ^ Class of associated type
             -> VarEnv Type     -- ^ Instantiation of class TyVars
             -> LTyClDecl Name  -- ^ RHS
-            -> TcM TyCon
+            -> TcM FamInst
 tcAssocDecl clas mini_env (L loc decl)
   = setSrcSpan loc      $
     tcAddDeclCtxt decl  $
-    do { at_tc <- tcFamInstDecl NotTopLevel decl
-       ; let Just (fam_tc, at_tys) = tyConFamInst_maybe at_tc
-  
+    do { fam_inst <- tcFamInstDecl NotTopLevel decl
+       ; let (fam_tc, at_tys) = famInstLHS fam_inst
+
        -- Check that the associated type comes from this class
        ; checkTc (Just clas == tyConAssoc_maybe fam_tc)
-                 (badATErr (className clas) (tyConName at_tc))
+                 (badATErr (className clas) (tyConName fam_tc))
 
        -- See Note [Checking consistent instantiation] in TcTyClsDecls
        ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys
 
-       ; return at_tc }
+       ; return fam_inst }
   where
     check_arg fam_tc_tv at_ty
       | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
       = checkTc (inst_ty `eqType` at_ty) 
                 (wrongATArgErr at_ty inst_ty)
+                -- No need to instantiate here, becuase the axiom
+                -- uses the same type variables as the assocated class
       | otherwise
       = return ()   -- Allow non-type-variable instantiation
                     -- See Note [Associated type instances]