Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- tcLookupImported_maybe :: Name -> TcM (MaybeErr MsgDoc TyThing)
- importDecl :: Name -> IfM lcl (MaybeErr MsgDoc TyThing)
- checkWiredInTyCon :: TyCon -> TcM ()
- tcHiBootIface :: HscSource -> Module -> TcRn SelfBootInfo
- typecheckIface :: ModIface -> IfG ModDetails
- typecheckIfacesForMerging :: Module -> [ModIface] -> IORef TypeEnv -> IfM lcl (TypeEnv, [ModDetails])
- typecheckIfaceForInstantiate :: NameShape -> ModIface -> IfM lcl ModDetails
- tcIfaceDecl :: Bool -> IfaceDecl -> IfL TyThing
- tcIfaceInst :: IfaceClsInst -> IfL ClsInst
- tcIfaceFamInst :: IfaceFamInst -> IfL FamInst
- tcIfaceRules :: Bool -> [IfaceRule] -> IfL [CoreRule]
- tcIfaceAnnotations :: [IfaceAnnotation] -> IfL [Annotation]
- tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch]
- tcIfaceExpr :: IfaceExpr -> IfL CoreExpr
- tcIfaceGlobal :: Name -> IfL TyThing

# Documentation

checkWiredInTyCon :: TyCon -> TcM () Source #

tcHiBootIface :: HscSource -> Module -> TcRn SelfBootInfo Source #

typecheckIface :: ModIface -> IfG ModDetails Source #

typecheckIfacesForMerging :: Module -> [ModIface] -> IORef TypeEnv -> IfM lcl (TypeEnv, [ModDetails]) Source #

This is a very interesting function. Like typecheckIface, we want to type check an interface file into a ModDetails. However, the use-case for these ModDetails is different: we want to compare all of the ModDetails to ensure they define compatible declarations, and then merge them together. So in particular, we have to take a different strategy for knot-tying: we first speculatively merge the declarations to get the "base" truth for what we believe the types will be (this is "type computation.") Then we read everything in relative to this truth and check for compatibility.

During the merge process, we may need to nondeterministically
pick a particular declaration to use, if multiple signatures define
the declaration (`mergeIfaceDecl`

). If, for all choices, there
are no type synonym cycles in the resulting merged graph, then
we can show that our choice cannot matter. Consider the
set of entities which the declarations depend on: by assumption
of acyclicity, we can assume that these have already been shown to be equal
to each other (otherwise merging will fail). Then it must
be the case that all candidate declarations here are type-equal
(the choice doesn't matter) or there is an inequality (in which
case merging will fail.)

Unfortunately, the choice can matter if there is a cycle. Consider the following merge:

signature H where { type A = C; type B = A; data C } signature H where { type A = (); data B; type C = B }

If we pick `type A = C`

as our representative, there will be
a cycle and merging will fail. But if we pick `type A = ()`

as
our representative, no cycle occurs, and we instead conclude
that all of the types are unit. So it seems that we either
(a) need a stronger acyclicity check which considers *all*
possible choices from a merge, or (b) we must find a selection
of declarations which is acyclic, and show that this is always
the "best" choice we could have made (ezyang conjectures this
is the case but does not have a proof). For now this is
not implemented.

It's worth noting that at the moment, a data constructor and a type synonym are never compatible. Consider:

signature H where { type Int=C; type B = Int; data C = Int} signature H where { export Prelude.Int; data B; type C = B; }

This will be rejected, because the reexported Int in the second signature (a proper data type) is never considered equal to a type synonym. Perhaps this should be relaxed, where a type synonym in a signature is considered implemented by a data type declaration which matches the reference of the type synonym.

typecheckIfaceForInstantiate :: NameShape -> ModIface -> IfM lcl ModDetails Source #

Typecheck a signature `ModIface`

under the assumption that we have
instantiated it under some implementation (recorded in `mi_semantic_module`

)
and want to check if the implementation fills the signature.

This needs to operate slightly differently than `typecheckIface`

because (1) we have a `NameShape`

, from the exports of the
implementing module, which we will use to give our top-level
declarations the correct `Name`

s even when the implementor
provided them with a reexport, and (2) we have to deal with
DFun silliness (see Note [rnIfaceNeverExported])

tcIfaceInst :: IfaceClsInst -> IfL ClsInst Source #

tcIfaceFamInst :: IfaceFamInst -> IfL FamInst Source #

tcIfaceAnnotations :: [IfaceAnnotation] -> IfL [Annotation] Source #

tcIfaceCompleteSigs :: [IfaceCompleteMatch] -> IfL [CompleteMatch] Source #