diff options
| author | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-10 18:03:09 -0400 |
|---|---|---|
| committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-07-10 19:54:53 -0400 |
| commit | 7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab (patch) | |
| tree | 436af01cc0c03bb1f4c5728124056429b21c4d7e /docs | |
| parent | cf67e59a90bcaba657a9f5db3d5defb6289c274f (diff) | |
| download | haskell-7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab.tar.gz | |
Note [Ordering of implicit variables]
This addresses #14808
[ci skip]
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 041cfb4e4e..678f75c0df 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -10606,14 +10606,35 @@ Here are the details: will have its type variables ordered as ``m, a, b, c``. +- If the type signature includes any kind annotations (either on variable + binders or as annotations on types), any variables used in kind + annotations come before any variables never used in kind annotations. + This rule is not recursive: if there is an annotation within an annotation, + then the variables used therein are on equal footing. Examples:: + + f :: Proxy (a :: k) -> Proxy (b :: j) -> () + -- as if f :: forall k j a b. ... + + g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> () + -- as if g :: forall j k b a. ... + -- NB: k is in a kind annotation within a kind annotation + - If any of the variables depend on other variables (that is, if some of the variables are *kind* variables), the variables are reordered so that kind variables come before type variables, preserving the left-to-right order as much as possible. That is, GHC performs a - stable topological sort on the variables. - - For example: if we have ``bar :: Proxy (a :: (j, k)) -> b``, then - the variables are ordered ``j``, ``k``, ``a``, ``b``. + stable topological sort on the variables. Examples:: + + h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> () + -- as if h :: forall j k a b. ... + + In this example, all of ``a``, ``j``, and ``k`` are considered kind + variables and will always be placed before ``b``, a lowly type variable. + (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears + lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first, + because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k`` + are not reordered with respect to eacho other, even though doing so would + not violate dependency conditions. - Visible type application is available to instantiate only user-specified type variables. This means that in ``data Proxy a = Proxy``, the unmentioned |