CoAxiom.lhs 19.5 KB
Newer Older
1 2 3 4 5 6
%
% (c) The University of Glasgow 2012
%

\begin{code}

7
{-# LANGUAGE GADTs, ScopedTypeVariables #-}
8 9 10 11 12

-- | Module for coercion axioms, used to represent type family instances
-- and newtypes

module CoAxiom (
13
       Branched, Unbranched, BranchIndex, BranchList(..),
14 15
       toBranchList, fromBranchList,
       toBranchedList, toUnbranchedList,
16 17
       brListLength, brListNth, brListMap, brListFoldr, brListMapM,
       brListFoldlM_, brListZipWith,
18

19
       CoAxiom(..), CoAxBranch(..), 
20 21 22

       toBranchedAxiom, toUnbranchedAxiom,
       coAxiomName, coAxiomArity, coAxiomBranches,
23
       coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
24 25 26 27 28
       coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomRole,
       coAxiomSingleBranch, coAxBranchTyVars, coAxBranchRoles,
       coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
       placeHolderIncomps,

29
       Role(..), fsFromRole,
30

31 32
       CoAxiomRule(..), Eqn,
       BuiltInSynFamily(..), trivialBuiltInFamily
33 34 35 36 37
       ) where 

import {-# SOURCE #-} TypeRep ( Type )
import {-# SOURCE #-} TyCon ( TyCon )
import Outputable
38
import FastString
39 40 41 42
import Name
import Unique
import Var
import Util
43
import Binary
44
import Pair
45 46
import BasicTypes
import Data.Typeable ( Typeable )
47
import SrcLoc
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
import qualified Data.Data as Data

#include "HsVersions.h"

\end{code}

Note [Coercion axiom branches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In order to allow type family instance groups, an axiom needs to contain an
ordered list of alternatives, called branches. The kind of the coercion built
from an axiom is determined by which index is used when building the coercion
from the axiom.

For example, consider the axiom derived from the following declaration:

type instance where
  F [Int] = Bool
  F [a]   = Double
  F (a b) = Char

This will give rise to this axiom:

axF :: {                                           F [Int] ~ Bool
       ; forall (a :: *).                          F [a]   ~ Double
       ; forall (k :: BOX) (a :: k -> *) (b :: k). F (a b) ~ Char
       }

The axiom is used with the AxiomInstCo constructor of Coercion. If we wish
to have a coercion showing that F (Maybe Int) ~ Char, it will look like

axF[2] <*> <Maybe> <Int> :: F (Maybe Int) ~ Char
-- or, written using concrete-ish syntax --
AxiomInstCo axF 2 [Refl *, Refl Maybe, Refl Int]

Note that the index is 0-based.

For type-checking, it is also necessary to check that no previous pattern
can unify with the supplied arguments. After all, it is possible that some
of the type arguments are lambda-bound type variables whose instantiation may
cause an earlier match among the branches. We wish to prohibit this behavior,
so the type checker rules out the choice of a branch where a previous branch
89
can unify. See also [Branched instance checking] in FamInstEnv.hs.
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110

For example, the following is malformed, where 'a' is a lambda-bound type
variable:

axF[2] <*> <a> <Bool> :: F (a Bool) ~ Char

Why? Because a might be instantiated with [], meaning that branch 1 should
apply, not branch 2. This is a vital consistency check; without it, we could
derive Int ~ Bool, and that is a Bad Thing.

Note [Branched axioms]
~~~~~~~~~~~~~~~~~~~~~~~
Although a CoAxiom has the capacity to store many branches, in certain cases,
we want only one. These cases are in data/newtype family instances, newtype
coercions, and type family instances declared with "type instance ...", not
"type instance where". Furthermore, these unbranched axioms are used in a
variety of places throughout GHC, and it would difficult to generalize all of
that code to deal with branched axioms, especially when the code can be sure
of the fact that an axiom is indeed a singleton. At the same time, it seems
dangerous to assume singlehood in various places through GHC.

111 112 113 114
The solution to this is to label a CoAxiom with a phantom type variable
declaring whether it is known to be a singleton or not. The list of branches
is stored using a special form of list, declared below, that ensures that the
type variable is accurate.
115 116 117 118 119 120 121

As of this writing (Dec 2012), it would not be appropriate to use a promoted
type as the phantom type, so we use empty datatypes. We wish to have GHC
remain compilable with GHC 7.2.1. If you are revising this code and GHC no
longer needs to remain compatible with GHC 7.2.x, then please update this
code to use promoted types.

122 123 124 125 126 127 128

%************************************************************************
%*                                                                      *
                    Branch lists
%*                                                                      *
%************************************************************************

129
\begin{code}
130 131
type BranchIndex = Int  -- The index of the branch in the list of branches
                        -- Counting from zero
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166

-- the phantom type labels
data Unbranched deriving Typeable
data Branched deriving Typeable

data BranchList a br where
  FirstBranch :: a -> BranchList a br
  NextBranch :: a -> BranchList a br -> BranchList a Branched

-- convert to/from lists
toBranchList :: [a] -> BranchList a Branched
toBranchList [] = pprPanic "toBranchList" empty
toBranchList [b] = FirstBranch b
toBranchList (h:t) = NextBranch h (toBranchList t)

fromBranchList :: BranchList a br -> [a]
fromBranchList (FirstBranch b) = [b]
fromBranchList (NextBranch h t) = h : (fromBranchList t)

-- convert from any BranchList to a Branched BranchList
toBranchedList :: BranchList a br -> BranchList a Branched
toBranchedList (FirstBranch b) = FirstBranch b
toBranchedList (NextBranch h t) = NextBranch h t

-- convert from any BranchList to an Unbranched BranchList
toUnbranchedList :: BranchList a br -> BranchList a Unbranched
toUnbranchedList (FirstBranch b) = FirstBranch b
toUnbranchedList _ = pprPanic "toUnbranchedList" empty

-- length
brListLength :: BranchList a br -> Int
brListLength (FirstBranch _) = 1
brListLength (NextBranch _ t) = 1 + brListLength t

-- lookup
167
brListNth :: BranchList a br -> BranchIndex -> a
168 169 170 171 172 173 174 175 176 177 178 179 180 181
brListNth (FirstBranch b) 0 = b
brListNth (NextBranch h _) 0 = h
brListNth (NextBranch _ t) n = brListNth t (n-1)
brListNth _ _ = pprPanic "brListNth" empty

-- map, fold
brListMap :: (a -> b) -> BranchList a br -> [b]
brListMap f (FirstBranch b) = [f b]
brListMap f (NextBranch h t) = f h : (brListMap f t)

brListFoldr :: (a -> b -> b) -> b -> BranchList a br -> b
brListFoldr f x (FirstBranch b) = f b x
brListFoldr f x (NextBranch h t) = f h (brListFoldr f x t)

182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
brListMapM :: Monad m => (a -> m b) -> BranchList a br -> m [b]
brListMapM f (FirstBranch b) = f b >>= \fb -> return [fb]
brListMapM f (NextBranch h t) = do { fh <- f h
                                   ; ft <- brListMapM f t
                                   ; return (fh : ft) }

brListFoldlM_ :: forall a b m br. Monad m
              => (a -> b -> m a) -> a -> BranchList b br -> m ()
brListFoldlM_ f z brs = do { _ <- go z brs
                           ; return () }
  where go :: forall br'. Monad m => a -> BranchList b br' -> m a
        go acc (FirstBranch b)  = f acc b
        go acc (NextBranch h t) = do { fh <- f acc h
                                     ; go fh t }

197 198 199 200 201 202 203 204 205 206 207
-- zipWith
brListZipWith :: (a -> b -> c) -> BranchList a br1 -> BranchList b br2 -> [c]
brListZipWith f (FirstBranch a) (FirstBranch b) = [f a b]
brListZipWith f (FirstBranch a) (NextBranch b _) = [f a b]
brListZipWith f (NextBranch a _) (FirstBranch b) = [f a b]
brListZipWith f (NextBranch a ta) (NextBranch b tb) = f a b : brListZipWith f ta tb

-- pretty-printing

instance Outputable a => Outputable (BranchList a br) where
  ppr = ppr . fromBranchList
208 209 210 211 212 213 214
\end{code}

%************************************************************************
%*                                                                      *
                    Coercion axioms
%*                                                                      *
%************************************************************************
215

216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
Note [Storing compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During axiom application, we need to be aware of which branches are compatible
with which others. The full explanation is in Note [Compatibility] in
FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on
the unification algorithm.) Although we could theoretically compute
compatibility on the fly, this is silly, so we store it in a CoAxiom.

Specifically, each branch refers to all other branches with which it is
incompatible. This list might well be empty, and it will always be for the
first branch of any axiom.

CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
stored in cab_incomps. The incompatibilities are properly a property of the
axiom as a whole, and they are computed only when the final axiom is built.

During serialization, the list is converted into a list of the indices
of the branches.

235
\begin{code}
236 237 238 239 240 241 242 243
-- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.

-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.lhs
data CoAxiom br
  = CoAxiom                   -- Type equality axiom.
    { co_ax_unique   :: Unique        -- unique identifier
    , co_ax_name     :: Name          -- name for pretty-printing
244
    , co_ax_role     :: Role          -- role of the axiom's equality
245 246 247 248 249 250 251 252 253 254 255
    , co_ax_tc       :: TyCon         -- the head of the LHS patterns
    , co_ax_branches :: BranchList CoAxBranch br
                                      -- the branches that form this axiom
    , co_ax_implicit :: Bool          -- True <=> the axiom is "implicit"
                                      -- See Note [Implicit axioms]
         -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1.
    }
  deriving Typeable

data CoAxBranch
  = CoAxBranch
256 257 258 259
    { cab_loc      :: SrcSpan       -- Location of the defining equation
                                    -- See Note [CoAxiom locations]
    , cab_tvs      :: [TyVar]       -- Bound type variables; not necessarily fresh
                                    -- See Note [CoAxBranch type variables]
260
    , cab_roles    :: [Role]        -- See Note [CoAxBranch roles]
261 262 263 264
    , cab_lhs      :: [Type]        -- Type patterns to match against
    , cab_rhs      :: Type          -- Right-hand side of the equality
    , cab_incomps  :: [CoAxBranch]  -- The previous incompatible branches
                                    -- See Note [Storing compatibility]
265 266 267 268
    }
  deriving Typeable

toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
269 270
toBranchedAxiom (CoAxiom unique name role tc branches implicit)
  = CoAxiom unique name role tc (toBranchedList branches) implicit
271 272

toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
273 274
toUnbranchedAxiom (CoAxiom unique name role tc branches implicit)
  = CoAxiom unique name role tc (toUnbranchedList branches) implicit
275

276 277 278
coAxiomNumPats :: CoAxiom br -> Int
coAxiomNumPats = length . coAxBranchLHS . (flip coAxiomNthBranch 0)

279 280 281
coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
coAxiomNthBranch (CoAxiom { co_ax_branches = bs }) index
  = brListNth bs index
282

283
coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
284 285 286 287 288 289
coAxiomArity ax index
  = length $ cab_tvs $ coAxiomNthBranch ax index

coAxiomName :: CoAxiom br -> Name
coAxiomName = co_ax_name

290 291 292
coAxiomRole :: CoAxiom br -> Role
coAxiomRole = co_ax_role

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
coAxiomBranches :: CoAxiom br -> BranchList CoAxBranch br
coAxiomBranches = co_ax_branches

coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches = branches })
  | FirstBranch br <- branches
  = Just br
  | otherwise
  = Nothing

coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (CoAxiom { co_ax_branches = FirstBranch br }) = br

coAxiomTyCon :: CoAxiom br -> TyCon
coAxiomTyCon = co_ax_tc

coAxBranchTyVars :: CoAxBranch -> [TyVar]
coAxBranchTyVars = cab_tvs

coAxBranchLHS :: CoAxBranch -> [Type]
coAxBranchLHS = cab_lhs

coAxBranchRHS :: CoAxBranch -> Type
coAxBranchRHS = cab_rhs

318 319 320
coAxBranchRoles :: CoAxBranch -> [Role]
coAxBranchRoles = cab_roles

321 322 323
coAxBranchSpan :: CoAxBranch -> SrcSpan
coAxBranchSpan = cab_loc

324 325
isImplicitCoAxiom :: CoAxiom br -> Bool
isImplicitCoAxiom = co_ax_implicit
326

327 328 329
coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
coAxBranchIncomps = cab_incomps

330
-- See Note [Compatibility checking] in FamInstEnv
331 332 333
placeHolderIncomps :: [CoAxBranch]
placeHolderIncomps = panic "placeHolderIncomps"

334 335
\end{code}

336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357
Note [CoAxBranch type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the case of a CoAxBranch of an associated type-family instance, 
we use the *same* type variables (where possible) as the
enclosing class or instance.  Consider
   class C a b where
     type F x b 
     type F [y] b = ...     -- Second param must be b

   instance C Int [z] where
     type F Int [z] = ...   -- Second param must be [z]

In the CoAxBranch in the instance decl (F Int [z]) we use the
same 'z', so that it's easy to check that that type is the same
as that in the instance header.  

Similarly in the CoAxBranch for the default decl for F in the
class decl, we use the same 'b' to make the same check easy.

So, unlike FamInsts, there is no expectation that the cab_tvs
are fresh wrt each other, or any other CoAxBranch.

358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
Note [CoAxBranch roles]
~~~~~~~~~~~~~~~~~~~~~~~
Consider this code:

  newtype Age = MkAge Int
  newtype Wrap a = MkWrap a

  convert :: Wrap Age -> Int
  convert (MkWrap (MkAge i)) = i

We want this to compile to:

  NTCo:Wrap :: forall a. Wrap a ~R a
  NTCo:Age  :: Age ~R Int
  convert = \x -> x |> (NTCo:Wrap[0] NTCo:Age[0])

But, note that NTCo:Age is at role R. Thus, we need to be able to pass
coercions at role R into axioms. However, we don't *always* want to be able to
do this, as it would be disastrous with type families. The solution is to
annotate the arguments to the axiom with roles, much like we annotate tycon
tyvars. Where do these roles get set? Newtype axioms inherit their roles from
the newtype tycon; family axioms are all at role N.

381 382 383 384 385 386 387 388 389 390 391 392 393 394
Note [CoAxiom locations]
~~~~~~~~~~~~~~~~~~~~~~~~
The source location of a CoAxiom is stored in two places in the
datatype tree. 
  * The first is in the location info buried in the Name of the
    CoAxiom. This span includes all of the branches of a branched
    CoAxiom.
  * The second is in the cab_loc fields of the CoAxBranches.  

In the case of a single branch, we can extract the source location of
the branch from the name of the CoAxiom. In other cases, we need an
explicit SrcSpan to correctly store the location of the equation
giving rise to the FamInstBranch.

395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431
Note [Implicit axioms]
~~~~~~~~~~~~~~~~~~~~~~
See also Note [Implicit TyThings] in HscTypes
* A CoAxiom arising from data/type family instances is not "implicit".
  That is, it has its own IfaceAxiom declaration in an interface file

* The CoAxiom arising from a newtype declaration *is* "implicit".
  That is, it does not have its own IfaceAxiom declaration in an
  interface file; instead the CoAxiom is generated by type-checking
  the newtype declaration

\begin{code}
instance Eq (CoAxiom br) where
    a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
    a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }

instance Ord (CoAxiom br) where
    a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
    a <  b = case (a `compare` b) of { LT -> True;  EQ -> False; GT -> False }
    a >= b = case (a `compare` b) of { LT -> False; EQ -> True;  GT -> True  }
    a >  b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True  }
    compare a b = getUnique a `compare` getUnique b

instance Uniquable (CoAxiom br) where
    getUnique = co_ax_unique

instance Outputable (CoAxiom br) where
    ppr = ppr . getName

instance NamedThing (CoAxiom br) where
    getName = co_ax_name

instance Typeable br => Data.Data (CoAxiom br) where
    -- don't traverse?
    toConstr _   = abstractConstr "CoAxiom"
    gunfold _ _  = error "gunfold"
    dataTypeOf _ = mkNoRepType "CoAxiom"
432 433
\end{code}

434 435 436 437 438 439
%************************************************************************
%*                                                                      *
                    Roles
%*                                                                      *
%************************************************************************

Simon Peyton Jones's avatar
Simon Peyton Jones committed
440
Roles are defined here to avoid circular dependencies.
441 442 443 444 445 446 447 448

\begin{code}

-- See Note [Roles] in Coercion
-- defined here to avoid cyclic dependency with Coercion
data Role = Nominal | Representational | Phantom
  deriving (Eq, Data.Data, Data.Typeable)

449 450 451 452 453 454 455 456
-- These names are slurped into the parser code. Changing these strings
-- will change the **surface syntax** that GHC accepts! If you want to
-- change only the pretty-printing, do some replumbing. See
-- mkRoleAnnotDecl in RdrHsSyn
fsFromRole :: Role -> FastString
fsFromRole Nominal          = fsLit "nominal"
fsFromRole Representational = fsLit "representational"
fsFromRole Phantom          = fsLit "phantom"
457

458
instance Outputable Role where
459
  ppr = ftext . fsFromRole
460 461 462 463 464 465 466 467 468 469 470 471

instance Binary Role where
  put_ bh Nominal          = putByte bh 1
  put_ bh Representational = putByte bh 2
  put_ bh Phantom          = putByte bh 3

  get bh = do tag <- getByte bh
              case tag of 1 -> return Nominal
                          2 -> return Representational
                          3 -> return Phantom
                          _ -> panic ("get Role " ++ show tag)

472 473 474
\end{code}


Simon Peyton Jones's avatar
Simon Peyton Jones committed
475 476 477 478 479 480
%************************************************************************
%*                                                                      *
                    CoAxiomRule
              Rules for building Evidence
%*                                                                      *
%************************************************************************
481

Simon Peyton Jones's avatar
Simon Peyton Jones committed
482
Conditional axioms.  The general idea is that a `CoAxiomRule` looks like this:
483 484 485

    forall as. (r1 ~ r2, s1 ~ s2) => t1 ~ t2

Simon Peyton Jones's avatar
Simon Peyton Jones committed
486
My intention is to reuse these for both (~) and (~#).
487
The short-term plan is to use this datatype to represent the type-nat axioms.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
488
In the longer run, it may be good to unify this and `CoAxiom`,
489 490 491 492 493 494 495 496 497 498 499 500 501
as `CoAxiom` is the special case when there are no assumptions.

\begin{code}
-- | A more explicit representation for `t1 ~ t2`.
type Eqn = Pair Type

-- | For now, we work only with nominal equality.
data CoAxiomRule = CoAxiomRule
  { coaxrName      :: FastString
  , coaxrTypeArity :: Int       -- number of type argumentInts
  , coaxrAsmpRoles :: [Role]    -- roles of parameter equations
  , coaxrRole      :: Role      -- role of resulting equation
  , coaxrProves    :: [Type] -> [Eqn] -> Maybe Eqn
Simon Peyton Jones's avatar
Simon Peyton Jones committed
502 503 504 505
        -- ^ coaxrProves returns @Nothing@ when it doesn't like
        -- the supplied arguments.  When this happens in a coercion
        -- that means that the coercion is ill-formed, and Core Lint
        -- checks for that.
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
  } deriving Typeable

instance Data.Data CoAxiomRule where
  -- don't traverse?
  toConstr _   = abstractConstr "CoAxiomRule"
  gunfold _ _  = error "gunfold"
  dataTypeOf _ = mkNoRepType "CoAxiomRule"

instance Uniquable CoAxiomRule where
  getUnique = getUnique . coaxrName

instance Eq CoAxiomRule where
  x == y = coaxrName x == coaxrName y

instance Ord CoAxiomRule where
  compare x y = compare (coaxrName x) (coaxrName y)

instance Outputable CoAxiomRule where
  ppr = ppr . coaxrName
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542


-- Type checking of built-in families
data BuiltInSynFamily = BuiltInSynFamily
  { sfMatchFam      :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
  , sfInteractTop   :: [Type] -> Type -> [Eqn]
  , sfInteractInert :: [Type] -> Type ->
                       [Type] -> Type -> [Eqn]
  }

-- Provides default implementations that do nothing.
trivialBuiltInFamily :: BuiltInSynFamily
trivialBuiltInFamily = BuiltInSynFamily
  { sfMatchFam      = \_ -> Nothing
  , sfInteractTop   = \_ _ -> []
  , sfInteractInert = \_ _ _ _ -> []
  }

543 544
\end{code}