diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2022-05-13 11:24:24 +0100 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-05-13 22:24:02 -0400 |
| commit | aed356e1b68b2201fa6e3c5bf14079f3f3366b44 (patch) | |
| tree | 1f8284818e2e4548467c0d763943f566f85e37d5 /compiler/GHC/Tc | |
| parent | 49af0e52e7f5cb123140682c7246be5ed46ba6a6 (diff) | |
| download | haskell-aed356e1b68b2201fa6e3c5bf14079f3f3366b44.tar.gz | |
Comments only around HsWrapper
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Types/Evidence.hs | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 837903a0f7..dfe332eb08 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -221,6 +221,8 @@ maybeTcSymCo NotSwapped co = co ************************************************************************ -} +-- We write wrap :: t1 ~> t2 +-- if wrap[ e::t1 ] :: t2 data HsWrapper = WpHole -- The identity coercion @@ -229,12 +231,17 @@ data HsWrapper -- -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) + -- + -- If wrap1 :: t2 ~> t3 + -- wrap2 :: t1 ~> t2 + --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3 | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) - -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ] - -- So note that if wrap1 :: exp_arg <= act_arg - -- wrap2 :: act_res <= exp_res - -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) + -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ] + -- So note that if e :: act_arg -> act_res + -- wrap1 :: exp_arg ~> act_arg + -- wrap2 :: act_res ~> exp_res + -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res) -- This isn't the same as for mkFunCo, but it has to be this way -- because we can't use 'sym' to flip around these HsWrappers -- The TcType is the "from" type of the first wrapper |