Update and clean-up the implmenation of GHC.TypeLits
authorIavor S. Diatchki <diatchki@galois.com>
Thu, 10 Oct 2013 02:22:35 +0000 (19:22 -0700)
committerIavor S. Diatchki <diatchki@galois.com>
Thu, 10 Oct 2013 02:26:41 +0000 (19:26 -0700)
* Replace class `SingI` with two separate classes: `KnownNat` and `KnownSymbol`

* Rename `magicSingId` to `magicDictId`.

* Simplify and clean-up the "magic" implementation.  This version makes
  a lot more sense, at least to me :-)

* Update notes about how it all works:

  Note [KnownNat & KnownSymbol and EvLit] explains the evidence for the
  built-in classes

  Note [magicDictId magic] explains how we coerce singleton values into
  dictionaries.  This is used to turn run-time integers and strings into
  Proxy singletons of unknwon type (using an existential).

compiler/basicTypes/MkId.lhs
compiler/basicTypes/MkId.lhs-boot
compiler/prelude/PrelNames.lhs
compiler/prelude/PrelRules.lhs
compiler/typecheck/TcEvidence.lhs
compiler/typecheck/TcInteract.lhs

index d398b3f..05a49ea 100644 (file)
@@ -35,7 +35,7 @@ module MkId (
         wiredInIds, ghcPrimIds,
         unsafeCoerceName, unsafeCoerceId, realWorldPrimId, 
         voidArgId, nullAddrId, seqId, lazyId, lazyIdKey,
         wiredInIds, ghcPrimIds,
         unsafeCoerceName, unsafeCoerceId, realWorldPrimId, 
         voidArgId, nullAddrId, seqId, lazyId, lazyIdKey,
-        coercionTokenId, magicSingIId,
+        coercionTokenId, magicDictId,
 
        -- Re-export error Ids
        module PrelRules
 
        -- Re-export error Ids
        module PrelRules
@@ -137,7 +137,7 @@ ghcPrimIds
     unsafeCoerceId,
     nullAddrId,
     seqId,
     unsafeCoerceId,
     nullAddrId,
     seqId,
-    magicSingIId,
+    magicDictId,
     coerceId,
     proxyHashId
     ]
     coerceId,
     proxyHashId
     ]
@@ -1038,14 +1038,14 @@ they can unify with both unlifted and lifted types.  Hence we provide
 another gun with which to shoot yourself in the foot.
 
 \begin{code}
 another gun with which to shoot yourself in the foot.
 
 \begin{code}
-lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName, coerceName, proxyName :: Name
+lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicDictName, coerceName, proxyName :: Name
 unsafeCoerceName  = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName      = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#")     nullAddrIdKey      nullAddrId
 seqName           = mkWiredInIdName gHC_PRIM (fsLit "seq")           seqIdKey           seqId
 realWorldName     = mkWiredInIdName gHC_PRIM (fsLit "realWorld#")    realWorldPrimIdKey realWorldPrimId
 lazyIdName        = mkWiredInIdName gHC_MAGIC (fsLit "lazy")         lazyIdKey           lazyId
 coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
 unsafeCoerceName  = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName      = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#")     nullAddrIdKey      nullAddrId
 seqName           = mkWiredInIdName gHC_PRIM (fsLit "seq")           seqIdKey           seqId
 realWorldName     = mkWiredInIdName gHC_PRIM (fsLit "realWorld#")    realWorldPrimIdKey realWorldPrimId
 lazyIdName        = mkWiredInIdName gHC_MAGIC (fsLit "lazy")         lazyIdKey           lazyId
 coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
-magicSingIName    = mkWiredInIdName gHC_PRIM (fsLit "magicSingI")    magicSingIKey magicSingIId
+magicDictName     = mkWiredInIdName gHC_PRIM (fsLit "magicDict")     magicDictKey magicDictId
 coerceName        = mkWiredInIdName gHC_PRIM (fsLit "coerce")        coerceKey          coerceId
 proxyName         = mkWiredInIdName gHC_PRIM (fsLit "proxy#")        proxyHashKey       proxyHashId
 \end{code}
 coerceName        = mkWiredInIdName gHC_PRIM (fsLit "coerce")        coerceKey          coerceId
 proxyName         = mkWiredInIdName gHC_PRIM (fsLit "proxy#")        proxyHashKey       proxyHashId
 \end{code}
@@ -1130,8 +1130,8 @@ lazyId = pcMiscPrelId lazyIdName ty info
 
 
 --------------------------------------------------------------------------------
 
 
 --------------------------------------------------------------------------------
-magicSingIId :: Id  -- See Note [magicSingIId magic]
-magicSingIId = pcMiscPrelId magicSingIName ty info
+magicDictId :: Id  -- See Note [magicDictId magic]
+magicDictId = pcMiscPrelId magicDictName ty info
   where
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
   ty   = mkForAllTys [alphaTyVar] alphaTy
   where
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
   ty   = mkForAllTys [alphaTyVar] alphaTy
@@ -1245,42 +1245,49 @@ lazyId is defined in GHC.Base, so we don't *have* to inline it.  If it
 appears un-applied, we'll end up just calling it.
 
 
 appears un-applied, we'll end up just calling it.
 
 
-Note [magicSingIId magic]
+Note [magicDictId magic]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The identifier `magicSIngI` is just a place-holder, which is used to
+The identifier `magicDict` is just a place-holder, which is used to
 implement a primitve that we cannot define in Haskell but we can write
 in Core.  It is declared with a place-holder type:
 
 implement a primitve that we cannot define in Haskell but we can write
 in Core.  It is declared with a place-holder type:
 
-    magicSingI :: forall a. a
+    magicDict :: forall a. a
 
 The intention is that the identifier will be used in a very specific way,
 
 The intention is that the identifier will be used in a very specific way,
-namely we add the following to the library:
+to create dictionaries for classes with a single method.  Consider a class
+like this:
 
 
-    withSingI :: Sing n -> (SingI n => a) -> a
-    withSingI x = magicSingI x ((\f -> f) :: () -> ())
+   class C a where
+     f :: T a
 
 
-The actual primitive is `withSingI`, and it uses its first argument
-(of type `Sing n`) as the evidece/dictionary in the second argument.
-This is done by adding a built-in rule to `prelude/PrelRules.hs`
-(see `match_magicSingI`), which works as follows:
+We are going to use `magicDict`, in conjunction with a built-in Prelude
+rule, to cast values of type `T a` into dictionaries for `C a`.  To do
+this, we define a function like this in the library:
 
 
-magicSingI @ (Sing n -> (() -> ()) -> (SingI n -> a) -> a)
-             x
-             (\f -> _)
+  data WrapC a b = WrapC (C a => Proxy a -> b)
 
 
----->
+  withT :: (C a => Proxy a -> b)
+        ->  T a -> Proxy a -> b
+  withT f x y = magicDict (WrapC f) x y
+
+The purpose of `WrapC` is to avoid having `f` instantiated.
+Also, it avoids impredicativity, because `magicDict`'s type
+cannot be instantiated with a forall.  The field of `WrapC` contains
+a `Proxy` parameter which is used to link the type of the constraint,
+`C a`, with the type of the `Wrap` value being made.
 
 
-\(f :: (SingI n -> a) -> a) -> f (cast x (newtypeCo n))
+Next, we add a built-in Prelude rule (see prelude/PrelRules.hs),
+which will replace the RHS of this definition with the appropriate
+definition in Core.  The rewrite rule works as follows:
+
+magicDict@t (wrap@a@b f) x y
+---->
+f (x `cast` co a) y
 
 
-The `newtypeCo` coercion is extracted from the `SingI` type constructor,
-which is available in the instantiation.  We are casting `Sing n` into `SingI n`,
-which is OK because `SingI` is a class with a single methid,
-and thus it is implemented as newtype.
+The `co` coercion is the newtype-coercion extracted from the type-class.
+The type class is obtain by looking at the type of wrap.
 
 
-The `(\f -> f)` parameter is there just so that we can avoid
-having to make up a new name for the lambda, it is completely
-changed by the rewrite.
 
 
 -------------------------------------------------------------
 
 
 -------------------------------------------------------------
index fe66599..d7adedb 100644 (file)
@@ -10,7 +10,7 @@ data DataConBoxer
 mkDataConWorkId :: Name -> DataCon -> Id
 mkPrimOpId      :: PrimOp -> Id
 
 mkDataConWorkId :: Name -> DataCon -> Id
 mkPrimOpId      :: PrimOp -> Id
 
-magicSingIId :: Id
+magicDictId :: Id
 \end{code}
 
 
 \end{code}
 
 
index a176cb6..7d15614 100644 (file)
@@ -294,7 +294,7 @@ basicKnownKeyNames
         randomClassName, randomGenClassName, monadPlusClassName,
 
         -- Type-level naturals
         randomClassName, randomGenClassName, monadPlusClassName,
 
         -- Type-level naturals
-        singIClassName,
+        knownNatClassName, knownSymbolClassName,
 
         -- Implicit parameters
         ipClassName,
 
         -- Implicit parameters
         ipClassName,
@@ -1137,8 +1137,10 @@ randomGenClassName  = clsQual rANDOM (fsLit "RandomGen") randomGenClassKey
 isStringClassName   = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
 
 -- Type-level naturals
 isStringClassName   = clsQual dATA_STRING (fsLit "IsString") isStringClassKey
 
 -- Type-level naturals
-singIClassName :: Name
-singIClassName      = clsQual gHC_TYPELITS (fsLit "SingI") singIClassNameKey
+knownNatClassName :: Name
+knownNatClassName     = clsQual gHC_TYPELITS (fsLit "KnownNat") knownNatClassNameKey
+knownSymbolClassName :: Name
+knownSymbolClassName  = clsQual gHC_TYPELITS (fsLit "KnownSymbol") knownSymbolClassNameKey
 
 -- Implicit parameters
 ipClassName :: Name
 
 -- Implicit parameters
 ipClassName :: Name
@@ -1260,9 +1262,13 @@ datatypeClassKey    = mkPreludeClassUnique 39
 constructorClassKey = mkPreludeClassUnique 40
 selectorClassKey    = mkPreludeClassUnique 41
 
 constructorClassKey = mkPreludeClassUnique 40
 selectorClassKey    = mkPreludeClassUnique 41
 
--- SingI: see Note [SingI and EvLit] in TcEvidence
-singIClassNameKey :: Unique
-singIClassNameKey       = mkPreludeClassUnique 42
+-- KnownNat: see Note [KnowNat & KnownSymbol and EvLit] in TcEvidence
+knownNatClassNameKey :: Unique
+knownNatClassNameKey = mkPreludeClassUnique 42
+
+-- KnownSymbol: see Note [KnownNat & KnownSymbol and EvLit] in TcEvidence
+knownSymbolClassNameKey :: Unique
+knownSymbolClassNameKey = mkPreludeClassUnique 43
 
 ghciIoClassKey :: Unique
 ghciIoClassKey = mkPreludeClassUnique 44
 
 ghciIoClassKey :: Unique
 ghciIoClassKey = mkPreludeClassUnique 44
@@ -1713,8 +1719,8 @@ checkDotnetResNameIdKey       = mkPreludeMiscIdUnique 154
 undefinedKey :: Unique
 undefinedKey                  = mkPreludeMiscIdUnique 155
 
 undefinedKey :: Unique
 undefinedKey                  = mkPreludeMiscIdUnique 155
 
-magicSingIKey :: Unique
-magicSingIKey              = mkPreludeMiscIdUnique 156
+magicDictKey :: Unique
+magicDictKey                  = mkPreludeMiscIdUnique 156
 
 coerceKey :: Unique
 coerceKey                     = mkPreludeMiscIdUnique 157
 
 coerceKey :: Unique
 coerceKey                     = mkPreludeMiscIdUnique 157
index 3b895d8..b6ded2e 100644 (file)
@@ -20,12 +20,11 @@ module PrelRules ( primOpRules, builtinRules ) where
 #include "HsVersions.h"
 #include "../includes/MachDeps.h"
 
 #include "HsVersions.h"
 #include "../includes/MachDeps.h"
 
-import {-# SOURCE #-} MkId ( mkPrimOpId, magicSingIId )
+import {-# SOURCE #-} MkId ( mkPrimOpId, magicDictId )
 
 import CoreSyn
 import MkCore
 import Id
 
 import CoreSyn
 import MkCore
 import Id
-import Var         (setVarType)
 import Literal
 import CoreSubst   ( exprIsLiteral_maybe )
 import PrimOp      ( PrimOp(..), tagToEnumKey )
 import Literal
 import CoreSubst   ( exprIsLiteral_maybe )
 import PrimOp      ( PrimOp(..), tagToEnumKey )
@@ -888,8 +887,8 @@ builtinRules
                    ru_nargs = 2, ru_try = \dflags _ _ -> match_eq_string dflags },
      BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
                    ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
                    ru_nargs = 2, ru_try = \dflags _ _ -> match_eq_string dflags },
      BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
                    ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
-     BuiltinRule { ru_name = fsLit "MagicSingI", ru_fn = idName magicSingIId,
-                   ru_nargs = 3, ru_try = \_ _ _ -> match_magicSingI }
+     BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = idName magicDictId,
+                   ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict }
      ]
  ++ builtinIntegerRules
 
      ]
  ++ builtinIntegerRules
 
@@ -1062,18 +1061,19 @@ match_inline (Type _ : e : _)
 match_inline _ = Nothing
 
 
 match_inline _ = Nothing
 
 
--- See Note [magicSingIId magic] in `basicTypes/MkId.lhs`
+-- See Note [magicDictId magic] in `basicTypes/MkId.lhs`
 -- for a description of what is going on here.
 -- for a description of what is going on here.
-match_magicSingI :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
-match_magicSingI (Type t : e : Lam b _ : _)
-  | ((_ : _ : fu : _),_)  <- splitFunTys t
-  , (sI_type,_)           <- splitFunTy fu
-  , Just (sI_tc,xs)       <- splitTyConApp_maybe sI_type
-  , Just (_,_,co)         <- unwrapNewTyCon_maybe sI_tc
-  = Just $ let f = setVarType b fu
-           in Lam f $ Var f `App` Cast e (mkSymCo (mkUnbranchedAxInstCo Representational co xs))
-
-match_magicSingI _ = Nothing
+match_magicDict :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
+match_magicDict [Type _, Var wrap `App` Type a `App` Type _ `App` f, x, y ]
+  | Just (fieldTy, _)   <- splitFunTy_maybe $ dropForAlls $ idType wrap
+  , Just (dictTy, _)    <- splitFunTy_maybe fieldTy
+  , Just dictTc         <- tyConAppTyCon_maybe dictTy
+  , Just (_,_,co)       <- unwrapNewTyCon_maybe dictTc
+  = Just
+  $ f `App` Cast x (mkSymCo (mkUnbranchedAxInstCo Representational co [a]))
+      `App` y
+
+match_magicDict _ = Nothing
 
 -------------------------------------------------
 -- Integer rules
 
 -------------------------------------------------
 -- Integer rules
index 09c0333..4af9120 100644 (file)
@@ -532,8 +532,8 @@ data EvTerm
                                  -- dictionaries, even though the former have no
                                  -- selector Id.  We count up from _0_
 
                                  -- dictionaries, even though the former have no
                                  -- selector Id.  We count up from _0_
 
-  | EvLit EvLit                  -- Dictionary for class "SingI" for type lits.
-                                 -- Note [SingI and EvLit]
+  | EvLit EvLit       -- Dictionary for KnownNat and KnownLit classes.
+                      -- Note [KnownNat & KnownSymbol and EvLit]
 
   | EvCoercible EvCoercible      -- Dictionary for "Coercible a b"
                                  -- Note [Coercible Instances]
 
   | EvCoercible EvCoercible      -- Dictionary for "Coercible a b"
                                  -- Note [Coercible Instances]
@@ -606,40 +606,57 @@ Conclusion: a new wanted coercion variable should be made mutable.
  from super classes will be "given" and hence rigid]
 
 
  from super classes will be "given" and hence rigid]
 
 
-Note [SingI and EvLit]
-~~~~~~~~~~~~~~~~~~~~~~
-A part of the type-level literals implementation is the class "SingI",
-which provides a "smart" constructor for defining singleton values.
-Here is the key stuff from GHC.TypeLits
+Note [KnownNat & KnownSymbol and EvLit]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A part of the type-level literals implementation are the classes
+"KnownNat" and "KnownLit", which provide a "smart" constructor for
+defining singleton values.  Here is the key stuff from GHC.TypeLits
 
 
-  class SingI n where
-    sing :: Sing n
+  class KnownNat (n :: Nat) where
+    natSing :: SNat n
 
 
-  data family Sing (n::k)
-  newtype instance Sing (n :: Nat)    = SNat Integer
-  newtype instance Sing (s :: Symbol) = SSym String
+  newtype SNat (n :: Nat) = SNat Integer
 
 Conceptually, this class has infinitely many instances:
 
 
 Conceptually, this class has infinitely many instances:
 
-  instance Sing 0       where sing = SNat 0
-  instance Sing 1       where sing = SNat 1
-  instance Sing 2       where sing = SNat 2
-  instance Sing "hello" where sing = SSym "hello"
+  instance KnownNat 0       where natSing = SNat 0
+  instance KnownNat 1       where natSing = SNat 1
+  instance KnownNat 2       where natSing = SNat 2
   ...
 
   ...
 
-In practice, we solve "SingI" predicates in the type-checker because we can't
-have infinately many instances.  The evidence (aka "dictionary")
-for "SingI (n :: Nat)" is of the form "EvLit (EvNum n)".
+In practice, we solve `KnownNat` predicates in the type-checker
+(see typecheck/TcInteract.hs) because we can't have infinately many instances.
+The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
 
 We make the following assumptions about dictionaries in GHC:
 
 We make the following assumptions about dictionaries in GHC:
-  1. The "dictionary" for classes with a single method---like SingI---is
+  1. The "dictionary" for classes with a single method---like `KnownNat`---is
      a newtype for the type of the method, so using a evidence amounts
      to a coercion, and
   2. Newtypes use the same representation as their definition types.
 
      a newtype for the type of the method, so using a evidence amounts
      to a coercion, and
   2. Newtypes use the same representation as their definition types.
 
-So, the evidence for "SingI" is just a value of the representation type,
-wrapped in two newtype constructors: one to make it into a "Sing" value,
-and another to make it into "SingI" evidence.
+So, the evidence for `KnownNat` is just a value of the representation type,
+wrapped in two newtype constructors: one to make it into a `SNat` value,
+and another to make it into a `KnownNat` dictionary.
+
+Also note that `natSing` and `SNat` are never actually exposed from the
+library---they are just an implementation detail.  Instead, users see
+a more convenient function, defined in terms of `natSing`:
+
+  natVal :: KnownNat n => proxy n -> Integer
+
+The reason we don't use this directly in the class is that it is simpler
+and more efficient to pass around an integer rather than an entier function,
+especialy when the `KnowNat` evidence is packaged up in an existential.
+
+The story for kind `Symbol` is analogous:
+  * class KnownSymbol
+  * newypte SSymbol
+  * Evidence: EvLit (EvStr n)
+
+
+
+
+
 
 
 \begin{code}
 
 
 \begin{code}
index 682f9f4..b87c5bd 100644 (file)
@@ -13,19 +13,17 @@ module TcInteract (
 
 #include "HsVersions.h"
 
 
 #include "HsVersions.h"
 
-
 import BasicTypes ()
 import TcCanonical
 import VarSet
 import Type
 import Unify
 import BasicTypes ()
 import TcCanonical
 import VarSet
 import Type
 import Unify
-import FamInstEnv
 import FamInst(TcBuiltInSynFamily(..))
 import InstEnv( lookupInstEnv, instanceDFunId )
 
 import Var
 import TcType
 import FamInst(TcBuiltInSynFamily(..))
 import InstEnv( lookupInstEnv, instanceDFunId )
 
 import Var
 import TcType
-import PrelNames (singIClassName, ipClassNameKey )
+import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
 import TysWiredIn ( coercibleClass )
 import Id( idType )
 import Class
 import TysWiredIn ( coercibleClass )
 import Id( idType )
 import Class
@@ -1734,47 +1732,41 @@ instance Outputable LookupInstResult where
 
 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
 
 
 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
 
-matchClassInst _ clas [ k, ty ] _
-  | className clas == singIClassName
+matchClassInst _ clas [ ty ] _
+  | className clas == knownNatClassName
   , Just n <- isNumLitTy ty = makeDict (EvNum n)
 
   , Just n <- isNumLitTy ty = makeDict (EvNum n)
 
-  | className clas == singIClassName
+  | className clas == knownSymbolClassName
   , Just s <- isStrLitTy ty = makeDict (EvStr s)
 
   where
   {- This adds a coercion that will convert the literal into a dictionary
   , Just s <- isStrLitTy ty = makeDict (EvStr s)
 
   where
   {- This adds a coercion that will convert the literal into a dictionary
-     of the appropriate type.  See Note [SingI and EvLit] in TcEvidence.
-     The coercion happens in 3 steps:
+     of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
+     in TcEvidence.  The coercion happens in 2 steps:
+
+     Integer -> SNat n     -- representation of literal to singleton
+     SNat n  -> KnownNat n -- singleton to dictionary
 
 
-     evLit    -> Sing_k_n   -- literal to representation of data family
-     Sing_k_n -> Sing k n   -- representation of data family to data family
-     Sing k n -> SingI k n   -- data family to class dictionary.
+     The process is mirrored for Symbols:
+     String    -> SSymbol n
+     SSymbol n -> KnownSymbol n
   -}
   makeDict evLit =
     case unwrapNewTyCon_maybe (classTyCon clas) of
   -}
   makeDict evLit =
     case unwrapNewTyCon_maybe (classTyCon clas) of
-      Just (_,dictRep, axDict)
-        | Just tcSing <- tyConAppTyCon_maybe dictRep ->
-           do mbInst <- matchOpenFam tcSing [k,ty]
-              case mbInst of
-                Just FamInstMatch
-                  { fim_instance = FamInst { fi_axiom  = axDataFam
-                                           , fi_flavor = DataFamilyInst tcon
-                                           }
-                  , fim_tys = tys
-                  } | Just (_,_,axSing) <- unwrapNewTyCon_maybe tcon ->
-                    -- co1 and co3 are at role R, while co2 is at role N.
-                    -- BUT, when desugaring to Coercions, the roles get fixed.
-                  do let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axSing tys
-                         co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDataFam tys
-                         co3 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [k,ty]
-                     return $ GenInst [] $ EvCast (EvLit evLit) $
-                        mkTcTransCo co1 $ mkTcTransCo co2 co3
-
-                _ -> unexpected
-
-      _ -> unexpected
-
-  unexpected = panicTcS (text "Unexpected evidence for SingI")
+      Just (_,_, axDict)
+        | [ meth ]   <- classMethods clas
+        , Just tcRep <- tyConAppTyCon_maybe -- SNat
+                      $ funResultTy         -- SNat n
+                      $ dropForAlls         -- KnownNat n => SNat n
+                      $ idType meth         -- forall n. KnownNat n => SNat n
+        , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
+        -> return $
+           let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axRep  [ty]
+               co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [ty]
+           in GenInst [] $ EvCast (EvLit evLit) (mkTcTransCo co1 co2)
+
+      _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
+                     $$ vcat (map (ppr . idType) (classMethods clas)))
 
 matchClassInst _ clas [ ty1, ty2 ] _
   | clas == coercibleClass =  do
 
 matchClassInst _ clas [ ty1, ty2 ] _
   | clas == coercibleClass =  do