Commit b2fa2d41 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Make type-level evaluation work with :kind!

The main change is to add a case to `reduceTyFamApp_maybe` to evaluate
built-in type constructors (e.g., (+), (*), and friends).

To avoid problems with recursive modules, I moved the definition of
TcBuiltInSynFamily from `FamInst` to `FamInstEnv`.  I am still not sure if
this is the right place.

There is also a wibble that it'd be nice to fix:

when we evaluate a built-in type function, using`sfMatchFam`, we get
a `TcCoercion`.  However, `reduceTyFamApp_maybe` needs a `Corecion`.
I couldn't find a nice way to convert between the two, so I resorted to
a bit of hack (marked with `XXX`).

The hack is that we happen to know that the built-in constructors for
the type-nat functions always return coercions of shape `TcAxiomRuleCo`,
with no assumptions, so it easy to convert `TcCoercion` to `Coercion`
in this one case.  This is enough to make things work, but it is clearly
a cludge.
parent 1c17d00f
......@@ -451,7 +451,7 @@ compiler_stage3_SplitObjs = NO
# We therefore need to split some of the modules off into a separate
# DLL. This clump are the modules reachable from DynFlags:
compiler_stage2_dll0_START_MODULE = DynFlags
compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes BinIface Binary Bitmap BlockId BooleanFormula BreakArray BufWrite BuildTyCl ByteCodeAsm ByteCodeInstr ByteCodeItbls CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreLint CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DsMonad DynFlags Encoding ErrUtils Exception ExtsCompat46 FamInst FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Finder Fingerprint FiniteMap ForeignCall Hooks Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes IOEnv Id IdInfo IfaceEnv IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal LoadIface Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic PipelineMonad Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelInfo PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcIface TcMType TcRnMonad TcRnTypes TcType TcTypeNats TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
compiler_stage2_dll0_MODULES = Annotations Avail Bag BasicTypes BinIface Binary Bitmap BlockId BooleanFormula BreakArray BufWrite BuildTyCl ByteCodeAsm ByteCodeInstr ByteCodeItbls CLabel Class CmdLineParser Cmm CmmCallConv CmmExpr CmmInfo CmmMachOp CmmNode CmmType CmmUtils CoAxiom CodeGen.Platform CodeGen.Platform.ARM CodeGen.Platform.NoRegs CodeGen.Platform.PPC CodeGen.Platform.PPC_Darwin CodeGen.Platform.SPARC CodeGen.Platform.X86 CodeGen.Platform.X86_64 Coercion Config Constants CoreArity CoreFVs CoreLint CoreSubst CoreSyn CoreTidy CoreUnfold CoreUtils CostCentre DataCon Demand Digraph DriverPhases DsMonad DynFlags Encoding ErrUtils Exception ExtsCompat46 FamInstEnv FastBool FastFunctions FastMutInt FastString FastTypes Finder Fingerprint FiniteMap ForeignCall Hooks Hoopl Hoopl.Dataflow HsBinds HsDecls HsDoc HsExpr HsImpExp HsLit HsPat HsSyn HsTypes HsUtils HscTypes IOEnv Id IdInfo IfaceEnv IfaceSyn IfaceType InstEnv InteractiveEvalTypes Kind ListSetOps Literal LoadIface Maybes MkCore MkGraph MkId Module MonadUtils Name NameEnv NameSet OccName OccurAnal OptCoercion OrdList Outputable PackageConfig Packages Pair Panic PipelineMonad Platform PlatformConstants PprCmm PprCmmDecl PprCmmExpr PprCore PrelInfo PrelNames PrelRules Pretty PrimOp RdrName Reg RegClass Rules SMRep Serialized SrcLoc StaticFlags StgCmmArgRep StgCmmClosure StgCmmEnv StgCmmLayout StgCmmMonad StgCmmProf StgCmmTicky StgCmmUtils StgSyn Stream StringBuffer TcEvidence TcIface TcRnMonad TcRnTypes TcType TcTypeNats TrieMap TyCon Type TypeRep TysPrim TysWiredIn Unify UniqFM UniqSet UniqSupply Unique Util Var VarEnv VarSet
compiler_stage2_dll0_HS_OBJS = \
$(patsubst %,compiler/stage2/build/%.$(dyn_osuf),$(subst .,/,$(compiler_stage2_dll0_MODULES)))
......
......@@ -13,11 +13,9 @@ module FamInst (
checkFamInstConsistency, tcExtendLocalFamInstEnv,
tcLookupFamInst,
tcGetFamInstEnvs,
newFamInst,
TcBuiltInSynFamily(..), trivialBuiltInFamily
newFamInst
) where
import Pair(Pair)
import HscTypes
import FamInstEnv
import InstEnv( roughMatchTcs )
......@@ -41,7 +39,6 @@ import VarSet
import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
import TcEvidence(TcCoercion)
#include "HsVersions.h"
\end{code}
......@@ -335,25 +332,3 @@ tcGetFamInstEnvs
; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
\end{code}
Type checking of built-in families
==================================
\begin{code}
data TcBuiltInSynFamily = TcBuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (TcCoercion, TcType)
, sfInteractTop :: [Type] -> Type -> [Pair TcType]
, sfInteractInert :: [Type] -> Type ->
[Type] -> Type -> [Pair TcType]
}
-- Provides default implementations that do nothing.
trivialBuiltInFamily :: TcBuiltInSynFamily
trivialBuiltInFamily = TcBuiltInSynFamily
{ sfMatchFam = \_ -> Nothing
, sfInteractTop = \_ _ -> []
, sfInteractInert = \_ _ _ _ -> []
}
\end{code}
......@@ -11,7 +11,7 @@ import TcCanonical
import VarSet
import Type
import Unify
import FamInst(TcBuiltInSynFamily(..))
import FamInstEnv(TcBuiltInSynFamily(..))
import InstEnv( lookupInstEnv, instanceDFunId )
import Var
......
......@@ -25,7 +25,7 @@ import PrelNames ( gHC_TYPELITS
, typeNatLeqTyFamNameKey
, typeNatSubTyFamNameKey
)
import FamInst ( TcBuiltInSynFamily(..) )
import FamInstEnv ( TcBuiltInSynFamily(..) )
import FastString ( FastString, fsLit )
import qualified Data.Map as Map
import Data.Maybe ( isJust )
......
......@@ -32,7 +32,10 @@ module FamInstEnv (
normaliseType, normaliseTcApp,
-- Flattening
flattenTys
flattenTys,
-- Built-in type families
TcBuiltInSynFamily(..), trivialBuiltInFamily
) where
#include "HsVersions.h"
......@@ -40,7 +43,8 @@ module FamInstEnv (
import InstEnv
import Unify
import Type
import TcType ( orphNamesOfTypes )
import TcType ( TcType, orphNamesOfTypes )
import TcEvidence (TcCoercion(TcAxiomRuleCo))
import TypeRep
import TyCon
import Coercion
......@@ -796,6 +800,16 @@ reduceTyFamApp_maybe envs role tc tys
ty = pSnd (coercionKind co)
in Just (args_co `mkTransCo` co, ty)
| Just ax <- isBuiltInSynFamTyCon_maybe tc
, Just (tcco,ty) <- sfMatchFam ax ntys
-- XXX: we have a TcCoercion, but we need a Coercion.
-- For the time being, we convert coercions in just this one special case
-- but something more general might be nice.
, TcAxiomRuleCo coax ts [] <- tcco
= let co = mkAxiomRuleCo coax ts []
in Just (args_co `mkTransCo` co, ty)
| otherwise
= Nothing
......@@ -1059,3 +1073,28 @@ allTyVarsInTy = go
go (LitTy {}) = emptyVarSet
\end{code}
Type checking of built-in families
==================================
\begin{code}
data TcBuiltInSynFamily = TcBuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (TcCoercion, TcType)
, sfInteractTop :: [Type] -> Type -> [Pair TcType]
, sfInteractInert :: [Type] -> Type ->
[Type] -> Type -> [Pair TcType]
}
-- Provides default implementations that do nothing.
trivialBuiltInFamily :: TcBuiltInSynFamily
trivialBuiltInFamily = TcBuiltInSynFamily
{ sfMatchFam = \_ -> Nothing
, sfInteractTop = \_ _ -> []
, sfInteractInert = \_ _ _ _ -> []
}
\end{code}
\begin{code}
module FamInst where
module FamInstEnv where
data TcBuiltInSynFamily
\end{code}
......@@ -96,7 +96,7 @@ module TyCon(
import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
import {-# SOURCE #-} DataCon ( DataCon, isVanillaDataCon )
import {-# SOURCE #-} FamInst ( TcBuiltInSynFamily )
import {-# SOURCE #-} FamInstEnv ( TcBuiltInSynFamily )
import Var
import Class
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment