[commit: ghc] type-nats: Some rules (partially) specifying that FromNat1 is injective. (1fa0796)

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : type-nats

http://hackage.haskell.org/trac/ghc/changeset/1fa0796114153d00b298d6b83e2725fef36790c7

>---------------------------------------------------------------

commit 1fa0796114153d00b298d6b83e2725fef36790c7
Author: Iavor S. Diatchki <[email protected]>
Date:   Sat Sep 22 11:43:42 2012 -0700

    Some rules (partially) specifying that FromNat1 is injective.

>---------------------------------------------------------------

 compiler/typecheck/TcTypeNatsRules.hs |   33 ++++++++++++++++++++++++++++++++-
 1 files changed, 32 insertions(+), 1 deletions(-)

diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs
index 8f82b50..2fdd852 100644
--- a/compiler/typecheck/TcTypeNatsRules.hs
+++ b/compiler/typecheck/TcTypeNatsRules.hs
@@ -15,6 +15,8 @@ import TysWiredIn ( typeNatAddTyCon
                   , typeNatExpTyCon
                   , typeNatLeqTyCon
                   , trueTy, falseTy
+                  , nat1Kind, zeroTy
+                  , fromNat1TyCon
                   )
 
 import Name     ( Name, mkWiredInName, BuiltInSyntax(..) )
@@ -60,9 +62,15 @@ mkExp a b = mkTyConApp typeNatExpTyCon [a,b]
 mkLeq :: Type -> Type -> Type
 mkLeq a b = mkTyConApp typeNatLeqTyCon [a,b]
 
+mkFromNat1 :: Type -> Type
+mkFromNat1 a = mkTyConApp fromNat1TyCon [a]
+
 natVars :: [TyVar]
 natVars = tyVarList typeNatKind
 
+nat1Vars :: [TyVar]
+nat1Vars = tyVarList nat1Kind
+
 mkBoolLiTy :: Bool -> Type
 mkBoolLiTy b = if b then trueTy else falseTy
 
@@ -204,9 +212,32 @@ widenRules =
   , (True, mkAx 54 "LeqExp2" (take 3 natVars)
       [ n2 <== a, mkExp a b === c ] (b <== c))
 
+
+  , (True, mkAx 60 "FromNat1_inj" (take 2 nat1Vars ++ take 1 (drop 2 natVars))
+      [ mkFromNat1 a1 === c, mkFromNat1 b1 === c] (a1 === b1))
+
+  {- This follows from the injectivity rule, when interacted with the
+     definition for `FromNat1`.  We have the explicit rule here
+     because this is the only function that has explicit user-defined
+     equations and so we have no support for interacting with
+     existing equations.   This could be removed if GHC knows about
+     injective type families. -}
+  , (True, mkAx 61 "FromNat1Zero" (take 1 nat1Vars)
+      [ mkFromNat1 a1 === n0 ] (a === zeroTy))
+
+  {- We also want:
+      forall (a :: Nat1) (b :: Nat).i
+      exists (c :: Nat1)
+        (FromNat1 a ~ b, 1 <= b) => (a ~ Succ c)
+
+    Currently this is implemented with some hand-written code in TcTypeNats.hs
+  -}
+
   ]
   where
-  a : b : c : x : y : z : _ = map mkTyVarTy natVars
+  a  : b  : c : x : y : z : _ = map mkTyVarTy natVars
+  a1 : b1 : _ = map mkTyVarTy nat1Vars
+  n0 = mkNumLitTy 0
   n1 = mkNumLitTy 1
   n2 = mkNumLitTy 2