Fix pretty-printing precedence for equality constraints

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

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 09caf8e..a7b0594 100644 (file)
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -13,6 +13,7 @@ module TyCon(
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),

+       AssocFamilyPermutation,

 
         -- ** Constructing TyCons
        mkAlgTyCon,
 
         -- ** Constructing TyCons
        mkAlgTyCon,

@@ -38,6 +39,7 @@ module TyCon(
         isCoercionTyCon, isCoercionTyCon_maybe,
         isForeignTyCon,
 
         isCoercionTyCon, isCoercionTyCon_maybe,
         isForeignTyCon,
 

+       isInjectiveTyCon,

        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
        isNewTyCon, isAbstractTyCon, isOpenTyCon,
         isUnLiftedTyCon,
        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
        isNewTyCon, isAbstractTyCon, isOpenTyCon,
         isUnLiftedTyCon,

@@ -54,7 +56,6 @@ module TyCon(
        tyConTyVars,
        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
        tyConFamilySize,
        tyConTyVars,
        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
        tyConFamilySize,

-       tyConSelIds,

        tyConStupidTheta,
        tyConArity,
        tyConClass_maybe,
        tyConStupidTheta,
        tyConArity,
        tyConClass_maybe,

@@ -92,6 +93,7 @@ import Maybes
 import Outputable
 import FastString
 import Constants
 import Outputable
 import FastString
 import Constants

+import Data.List( elemIndex )

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

@@ -112,7 +114,7 @@ import Constants
 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
 --
 -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where
 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
 --
 -- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where

---    that type has kind @t1 :=: t2@. See "Coercion" for more on this
+--    that type has kind @t1 ~ t2@. See "Coercion" for more on this

 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.
 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.

@@ -144,8 +146,6 @@ data TyCon
                                        --
                                        -- Note that it does /not/ scope over the data constructors.
 
                                        --
                                        -- Note that it does /not/ scope over the data constructors.
 

-       algTcSelIds :: [Id],            -- ^ The record selectors of this type (possibly emptys)
-

        algTcGadtSyntax  :: Bool,       -- ^ Was the data type declared with GADT syntax? If so,
                                        -- that doesn't mean it's a true GADT; only that the "where"
                                        --      form was used. This field is used only to guide
        algTcGadtSyntax  :: Bool,       -- ^ Was the data type declared with GADT syntax? If so,
                                        -- that doesn't mean it's a true GADT; only that the "where"
                                        --      form was used. This field is used only to guide

@@ -211,7 +211,7 @@ data TyCon
        tyConExtName :: Maybe FastString        -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
     }
 
        tyConExtName :: Maybe FastString        -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
     }
 

-  -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@.
+  -- | Type coercions, such as @(~)@, @sym@, @trans@, @left@ and @right@.

   -- INVARIANT: coercions are always fully applied
   | CoercionTyCon {    
        tyConUnique :: Unique,
   -- INVARIANT: coercions are always fully applied
   | CoercionTyCon {    
        tyConUnique :: Unique,

@@ -260,17 +260,7 @@ data AlgTyConRhs
   -- >   data T b :: *
 
   | OpenTyCon {
   -- >   data T b :: *
 
   | OpenTyCon {

-
-      otArgPoss   :: Maybe [Int]
-       -- ^ @Nothing@ iff this is a top-level indexed type family.
-       -- @Just ns@ iff this is an associated (not top-level) family
-       --
-       -- In the latter case, for each 'TyVar' in the associated type declaration, 
-       -- @ns@ gives the position of that tyvar in the class argument list (starting 
-       -- from 0).
-       --
-       -- NB: The length of this list is less than the accompanying 'tyConArity' iff 
-       -- we have a higher kind signature.
+      otArgPoss :: AssocFamilyPermutation

     }
 
   -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 
     }
 
   -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 

@@ -316,6 +306,18 @@ data AlgTyConRhs
                                -- again check Trac #1072.
     }
 
                                -- again check Trac #1072.
     }
 

+type AssocFamilyPermutation
+  = Maybe [Int]  -- Nothing for *top-level* type families
+                 -- For *associated* type families, gives the position
+                -- of that 'TyVar' in the class argument list (0-indexed)
+                -- e.g.  class C a b c where { type F c a :: *->* }
+                 --       Then we get Just [2,0]
+        -- For *synonyms*, the length of the list is identical to
+        --                 the TyCon's arity
+        -- For *data types*, the length may be smaller than the
+        --     TyCon's arity; e.g. class C a where { data D a :: *->* }
+        --                    here D gets arity 2
+

 -- | Extract those 'DataCon's that we are able to learn about. Note that visibility in this sense does not
 -- correspond to visibility in the context of any particular user program!
 visibleDataCons :: AlgTyConRhs -> [DataCon]
 -- | Extract those 'DataCon's that we are able to learn about. Note that visibility in this sense does not
 -- correspond to visibility in the context of any particular user program!
 visibleDataCons :: AlgTyConRhs -> [DataCon]

@@ -369,16 +371,10 @@ okParent _       (FamilyTyCon fam_tc tys _co_tc) = tyConArity fam_tc == length t
 
 -- | Information pertaining to the expansion of a type synonym (@type@)
 data SynTyConRhs
 
 -- | Information pertaining to the expansion of a type synonym (@type@)
 data SynTyConRhs

-  = OpenSynTyCon Kind          
-                (Maybe [Int])  -- ^ A Type family synonym. The /result/ 'Kind' is
-                               -- given for associated families, and in this case the
-                               -- list of @Int@s is not empty, and for each 'TyVar' in
-                               -- the associated type declaration, it gives the position
-                               -- of that 'TyVar' in the class argument list (starting
-                               -- from 0). 
-                               --
-                               -- NB: The length of this list will be less than 'tyConArity' iff
-                               -- the family has a higher kind signature.
+  = OpenSynTyCon      -- e.g. type family F x y :: * -> *
+       Kind          -- Kind of the "rhs"; ie *excluding type indices*
+                             --     In the example, the kind is (*->*)
+       AssocFamilyPermutation

 
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some
 
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some

@@ -393,7 +389,7 @@ newtype, to the newtype itself. For example,
 
    newtype T a = MkT (a -> a)
 
 
    newtype T a = MkT (a -> a)
 

-the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t ->
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t ->

 t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
 own; it basically has its own typing rule for the fully-applied
 version.  If the newtype T has k type variables then CoT has arity at
 t.  This TyCon is a CoercionTyCon, so it does not have a kind on its
 own; it basically has its own typing rule for the fully-applied
 version.  If the newtype T has k type variables then CoT has arity at

@@ -403,11 +399,11 @@ ending with the same type variables as the left hand side, we
 
    newtype S a = MkT [a]
 
 
    newtype S a = MkT [a]
 

-then we would generate the arity 0 coercion CoS : S :=: [].  The
+then we would generate the arity 0 coercion CoS : S ~ [].  The

 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write
 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write

-       axiom CoT : (forall t. T t) :=: (forall t. [t])
+       axiom CoT : (forall t. T t) ~ (forall t. [t])

 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])

@@ -418,7 +414,7 @@ be saturated, but which encodes as
        TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like
        TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like

-       axiom CoT t :  T t :=: [t]
+       axiom CoT t :  T t ~ [t]

 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~

@@ -499,7 +495,7 @@ Then
 %************************************************************************
 
 A PrimRep is somewhat similar to a CgRep (see codeGen/SMRep) and a
 %************************************************************************
 
 A PrimRep is somewhat similar to a CgRep (see codeGen/SMRep) and a

-MachRep (see cmm/MachOp), although each of these types has a distinct
+MachRep (see cmm/CmmExpr), although each of these types has a distinct

 and clearly defined purpose:
 
   - A PrimRep is a CgRep + information about signedness + information
 and clearly defined purpose:
 
   - A PrimRep is a CgRep + information about signedness + information

@@ -576,13 +572,12 @@ mkAlgTyCon :: Name
            -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'. Arity is inferred from the length of this list
            -> [PredType]        -- ^ Stupid theta: see 'algTcStupidTheta'
            -> AlgTyConRhs       -- ^ Information about dat aconstructors
            -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'. Arity is inferred from the length of this list
            -> [PredType]        -- ^ Stupid theta: see 'algTcStupidTheta'
            -> AlgTyConRhs       -- ^ Information about dat aconstructors

-           -> [Id]              -- ^ Selector 'Id's

            -> TyConParent
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Does it have generic functions? See 'hasGenerics'
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
            -> TyCon
            -> TyConParent
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Does it have generic functions? See 'hasGenerics'
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
            -> TyCon

-mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn
+mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn

   = AlgTyCon { 
        tyConName        = name,
        tyConUnique      = nameUnique name,
   = AlgTyCon { 
        tyConName        = name,
        tyConUnique      = nameUnique name,

@@ -591,7 +586,6 @@ mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
        algTcRhs         = rhs,
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
        algTcRhs         = rhs,

-       algTcSelIds      = sel_ids,

        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,
        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,

@@ -601,7 +595,7 @@ mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn
 -- | Simpler specialization of 'mkAlgTyCon' for classes
 mkClassTyCon :: Name -> Kind -> [TyVar] -> AlgTyConRhs -> Class -> RecFlag -> TyCon
 mkClassTyCon name kind tyvars rhs clas is_rec =
 -- | Simpler specialization of 'mkAlgTyCon' for classes
 mkClassTyCon :: Name -> Kind -> [TyVar] -> AlgTyConRhs -> Class -> RecFlag -> TyCon
 mkClassTyCon name kind tyvars rhs clas is_rec =

-  mkAlgTyCon name kind tyvars [] rhs [] (ClassTyCon clas) is_rec False False
+  mkAlgTyCon name kind tyvars [] rhs (ClassTyCon clas) is_rec False False

 
 mkTupleTyCon :: Name 
              -> Kind    -- ^ Kind of the resulting 'TyCon'
 
 mkTupleTyCon :: Name 
              -> Kind    -- ^ Kind of the resulting 'TyCon'

@@ -818,9 +812,20 @@ isEnumerationTyCon _                                                   = False
 
 -- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear?
 isOpenTyCon :: TyCon -> Bool
 
 -- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear?
 isOpenTyCon :: TyCon -> Bool

-isOpenTyCon (SynTyCon {synTcRhs = OpenSynTyCon _ _}) = True
-isOpenTyCon (AlgTyCon {algTcRhs = OpenTyCon {}    }) = True
-isOpenTyCon _                                       = False
+isOpenTyCon (SynTyCon {synTcRhs = OpenSynTyCon {}}) = True
+isOpenTyCon (AlgTyCon {algTcRhs = OpenTyCon {}})    = True
+isOpenTyCon _                                      = False
+
+-- | Injective 'TyCon's can be decomposed, so that
+--     T ty1 ~ T ty2  =>  ty1 ~ ty2
+isInjectiveTyCon :: TyCon -> Bool
+isInjectiveTyCon tc = not (isSynTyCon tc)
+       -- Ultimately we may have injective associated types
+        -- in which case this test will become more interesting
+       --
+       -- It'd be unusual to call isInjectiveTyCon on a regular H98
+       -- type synonym, because you should probably have expanded it first
+       -- But regardless, it's not injective!

 
 -- | Extract the mapping from 'TyVar' indexes to indexes in the corresponding family
 -- argument lists form an open 'TyCon' of any sort, if the given 'TyCon' is indeed
 
 -- | Extract the mapping from 'TyVar' indexes to indexes in the corresponding family
 -- argument lists form an open 'TyCon' of any sort, if the given 'TyCon' is indeed

@@ -836,14 +841,22 @@ assocTyConArgPoss_maybe _ = Nothing
 isTyConAssoc :: TyCon -> Bool
 isTyConAssoc = isJust . assocTyConArgPoss_maybe
 
 isTyConAssoc :: TyCon -> Bool
 isTyConAssoc = isJust . assocTyConArgPoss_maybe
 

--- | Sets up a 'TyVar' to family argument-list mapping in the given 'TyCon' if it is
--- an open 'TyCon'. Panics otherwise
-setTyConArgPoss :: TyCon -> [Int] -> TyCon
-setTyConArgPoss tc@(AlgTyCon { algTcRhs = rhs })               poss = 
-  tc { algTcRhs = rhs {otArgPoss = Just poss} }
-setTyConArgPoss tc@(SynTyCon { synTcRhs = OpenSynTyCon ki _ }) poss = 
-  tc { synTcRhs = OpenSynTyCon ki (Just poss) }
-setTyConArgPoss tc _ = pprPanic "setTyConArgPoss" (ppr tc)
+-- | Set the AssocFamilyPermutation structure in an 
+-- associated data or type synonym.  The [TyVar] are the
+-- class type variables.  Remember, the tyvars of an associated
+-- data/type are a subset of the class tyvars; except that an
+-- associated data type can have extra type variables at the
+-- end (see Note [Avoid name clashes for associated data types] in TcHsType)
+setTyConArgPoss :: [TyVar] -> TyCon -> TyCon
+setTyConArgPoss clas_tvs tc
+  = case tc of
+      AlgTyCon { algTcRhs = rhs }               -> tc { algTcRhs = rhs {otArgPoss = Just ps} }
+      SynTyCon { synTcRhs = OpenSynTyCon ki _ } -> tc { synTcRhs = OpenSynTyCon ki (Just ps) }
+      _                                         -> pprPanic "setTyConArgPoss" (ppr tc)
+  where
+    ps = catMaybes [tv `elemIndex` clas_tvs | tv <- tyConTyVars tc]
+       -- We will get Nothings for the "extra" type variables in an
+       -- associated data type

 
 -- The unit tycon didn't used to be classed as a tuple tycon
 -- but I thought that was silly so I've undone it
 
 -- The unit tycon didn't used to be classed as a tuple tycon
 -- but I thought that was silly so I've undone it

@@ -953,7 +966,7 @@ tcExpandTyCon_maybe _ _ = Nothing
 
 -- ^ Used to create the view /Core/ has on 'TyCon's. We expand not only closed synonyms like 'tcExpandTyCon_maybe',
 -- but also non-recursive @newtype@s
 
 -- ^ Used to create the view /Core/ has on 'TyCon's. We expand not only closed synonyms like 'tcExpandTyCon_maybe',
 -- but also non-recursive @newtype@s

-coreExpandTyCon_maybe (AlgTyCon {algTcRec = NonRecursive,      -- Not recursive
+coreExpandTyCon_maybe (AlgTyCon {

          algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs, nt_co = Nothing }}) tys
    = case etad_rhs of  -- Don't do this in the pattern match, lest we accidentally
                        -- match the etad_rhs of a *recursive* newtype
          algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs, nt_co = Nothing }}) tys
    = case etad_rhs of  -- Don't do this in the pattern match, lest we accidentally
                        -- match the etad_rhs of a *recursive* newtype

@@ -1007,11 +1020,6 @@ tyConFamilySize (AlgTyCon   {algTcRhs = OpenTyCon {}})                 = 0
 tyConFamilySize (TupleTyCon {})                                               = 1
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
 
 tyConFamilySize (TupleTyCon {})                                               = 1
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
 

--- | Extract the record selector 'Id's from an algebraic 'TyCon' and returns the empty list otherwise
-tyConSelIds :: TyCon -> [Id]
-tyConSelIds (AlgTyCon {algTcSelIds = fs}) = fs
-tyConSelIds _                             = []
-

 -- | Extract an 'AlgTyConRhs' with information about data constructors from an algebraic or tuple
 -- 'TyCon'. Panics for any other sort of 'TyCon'
 algTyConRhs :: TyCon -> AlgTyConRhs
 -- | Extract an 'AlgTyConRhs' with information about data constructors from an algebraic or tuple
 -- 'TyCon'. Panics for any other sort of 'TyCon'
 algTyConRhs :: TyCon -> AlgTyConRhs