[commit: ghc] master: Document Typeable's treatment of kind polymorphic tycons (6de1a5a)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/6de1a5a96cdaba080570e9f47ff8711796e2e83b/ghc

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

commit 6de1a5a96cdaba080570e9f47ff8711796e2e83b
Author: Ben Gamari <bgamari.foss at gmail.com>
Date:   Mon Sep 25 18:33:06 2017 -0400

    Document Typeable's treatment of kind polymorphic tycons
    
    Test Plan: Read it
    
    Reviewers: dfeuer, goldfire, austin, hvr
    
    Reviewed By: dfeuer
    
    Subscribers: rwbarton, thomie
    
    GHC Trac Issues: #14199
    
    Differential Revision: https://phabricator.haskell.org/D3991


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

6de1a5a96cdaba080570e9f47ff8711796e2e83b
 libraries/base/Data/Typeable/Internal.hs | 53 ++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index ff53921..d876a2b 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -32,6 +32,11 @@
 -----------------------------------------------------------------------------
 
 module Data.Typeable.Internal (
+    -- * Typeable and kind polymorphism
+    --
+    -- #kind_instantiation
+
+    -- * Miscellaneous
     Fingerprint(..),
 
     -- * Typeable class
@@ -690,3 +695,51 @@ mkTrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
 mkTrFun arg res = TrFun fpr arg res
   where fpr = fingerprintFingerprints [ typeRepFingerprint arg
                                       , typeRepFingerprint res]
+
+{- $kind_instantiation
+
+Consider a type like 'Data.Proxy.Proxy',
+
+@
+data Proxy :: forall k. k -> Type
+@
+
+One might think that one could decompose an instantiation of this type like
+ at Proxy Int@ into two applications,
+
+@
+'App' (App a b) c === typeRep @(Proxy Int)
+@
+
+where,
+
+@
+a = typeRep @Proxy
+b = typeRep @Type
+c = typeRep @Int
+@
+
+However, this isn't the case. Instead we can only decompose into an application
+and a constructor,
+
+@
+'App' ('Con' proxyTyCon) (typeRep @Int) === typeRep @(Proxy Int)
+@
+
+The reason for this is that 'Typeable' can only represent /kind-monomorphic/
+types. That is, we must saturate enough of @Proxy@\'s arguments to
+fully determine its kind. In the particular case of @Proxy@ this means we must
+instantiate the kind variable @k@ such that no @forall at -quantified variables
+remain.
+
+While it is not possible to decompose the 'Con' above into an application, it is
+possible to observe the kind variable instantiations of the constructor with the
+'Con\'' pattern,
+
+@
+'App' (Con' proxyTyCon kinds) _ === typeRep @(Proxy Int)
+@
+
+Here @kinds@ will be @[typeRep \@Type]@.
+
+-}