Make type-level evaluation work with :kind!
authorIavor S. Diatchki <diatchki@galois.com>
Wed, 13 Nov 2013 00:36:23 +0000 (16:36 -0800)
committerIavor S. Diatchki <diatchki@galois.com>
Wed, 13 Nov 2013 00:36:23 +0000 (16:36 -0800)
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.

compiler/ghc.mk
compiler/typecheck/FamInst.lhs
compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcTypeNats.hs
compiler/types/FamInstEnv.lhs
compiler/types/FamInstEnv.lhs-boot [moved from compiler/typecheck/FamInst.lhs-boot with 67% similarity]
compiler/types/TyCon.lhs

index a5a2034..f1eb535 100644 (file)
@@ -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)))
index 47cdfa9..ef47667 100644 (file)
@@ -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}
-
-
index 88ebfdb..2b742b2 100644 (file)
@@ -11,7 +11,7 @@ import TcCanonical
 import VarSet
 import Type
 import Unify
-import FamInst(TcBuiltInSynFamily(..))
+import FamInstEnv(TcBuiltInSynFamily(..))
 import InstEnv( lookupInstEnv, instanceDFunId )
 
 import Var
index 7f8c722..fe4a25d 100644 (file)
@@ -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 )
index 54de39c..89805de 100644 (file)
@@ -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}
+
+
similarity index 67%
rename from compiler/typecheck/FamInst.lhs-boot
rename to compiler/types/FamInstEnv.lhs-boot
index 6e4bd1d..4540148 100644 (file)
@@ -1,5 +1,5 @@
 \begin{code}
-module FamInst where
+module FamInstEnv where
 
 data TcBuiltInSynFamily
 \end{code}
index d9b3a85..f8667b0 100644 (file)
@@ -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