[commit: ghc] master: Add comments on Typeable (n :: Nat) (7ce6f64)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/7ce6f642a2806c425ba21d48a077d997703cf25b/ghc

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

commit 7ce6f642a2806c425ba21d48a077d997703cf25b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Jul 3 08:50:19 2018 +0100

    Add comments on Typeable (n :: Nat)
    
    See Note [Typeable for Nat and Symbol] in TcInteract,
    which I added after discussion on Trac #15322


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

7ce6f642a2806c425ba21d48a077d997703cf25b
 compiler/deSugar/DsBinds.hs      |  3 ++-
 compiler/typecheck/TcInteract.hs | 25 +++++++++++++++++++++++--
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index bec68b0..db7acfd 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -1279,7 +1279,8 @@ ds_ev_typeable ty (EvTypeableTrFun ev1 ev2)
        }
 
 ds_ev_typeable ty (EvTypeableTyLit ev)
-  = do { fun  <- dsLookupGlobalId tr_fun
+  = -- See Note [Typeable for Nat and Symbol] in TcInteract
+    do { fun  <- dsLookupGlobalId tr_fun
        ; dict <- dsEvTerm ev       -- Of type KnownNat/KnownSym
        ; let proxy = mkTyApps (Var proxyHashId) [ty_kind, ty]
        ; return (mkApps (mkTyApps (Var fun) [ty]) [ dict, proxy ]) }
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 97d1dde..5d3a988 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -2882,8 +2882,8 @@ mk_typeable_pred :: Class -> Type -> PredType
 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
 
   -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
-  -- we generate a sub-goal for the appropriate class. See #10348 for what
-  -- happens when we fail to do this.
+  -- we generate a sub-goal for the appropriate class.
+  -- See Note [Typeable for Nat and Symbol]
 doTyLit :: Name -> Type -> TcS LookupInstResult
 doTyLit kc t = do { kc_clas <- tcLookupClass kc
                   ; let kc_pred    = mkClassPred kc_clas [ t ]
@@ -2930,6 +2930,27 @@ a TypeRep for them.  For qualified but not polymorphic types, like
    at the current state of affairs this would be an odd exception as
    no other class works with impredicative types.
    For now we leave it off, until we have a better story for impredicativity.
+
+
+Note [Typeable for Nat and Symbol]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have special Typeable instances for Nat and Symbol.  Roughly we
+have this instance, implemented here by doTyLit:
+      instance KnownNat n => Typeable (n :: Nat) where
+         typeRep = tyepNatTypeRep @n
+where
+   Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a
+
+Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
+runtime value 'n'; it turns it into a string with 'show' and uses
+that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
+See #10348.
+
+Because of this rule it's inadvisable (see #15322) to have a constraint
+    f :: (Typeable (n :: Nat)) => blah
+in a function signature; it gives rise to overlap problems just as
+if you'd written
+    f :: Eq [a] => blah
 -}
 
 {- ********************************************************************