Richard Ben and I concluded 1. Currently saturated (->) is treated differently to unsaturated (->), as witnessed by the special kinding rule for FunTy. The shortest path for TypeRep is to do the same: add TrFunTy. 1. Moreover we probably need FunCo for coercions; at the moment it's done with TyConAppCo, but that doesn't work with (->) :: * -> * -> *. Having FunCo would be (a) more efficient for a very common case, (b) deal with the kinding issue. 2. splitAppTy_maybe currently will split a FunTy even when it is not used at kind *. This is probably wrong. Maybe it should return Nothing in the non-* case. Ben is trying this out. 3. Orthogonally, one could imagine generalising the kind of prefix (->) to (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type LiftedPtrRep Then FunTy would become an abbreviation/optimisation, to avoid a plethora of runtime-rep args. And splitAppTy_maybe could succeed all the time on FunTy. Ben is trying this. 4. Under (3) at what kinds is ((->) ?? LiftedPtrRep (Ord Int) Char) called? If we continue to distinguish * from Constraint, we'd need to instantiate ?? with ConstraintRep, and define type Constraint = TYPE ConstraintRep Orthogonally, one might wonder about combining * and Constraint, but we don't yet know how to do that well. | -----Original Message----- | From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] | Sent: 06 October 2016 15:08 | To: Ben Gamari <ben@smart-cactus.org> | Cc: Simon Peyton Jones <simonpj@microsoft.com> | Subject: Re: Typeable meeting | | Just seeing this now. (Please use my new address: rae@cs.brynmawr.edu). I | wasn't available yesterday at that time, anyway. | | Any conclusions reached? | | > On Oct 4, 2016, at 5:39 PM, Ben Gamari <ben@smart-cactus.org> wrote: | > | > Simon Peyton Jones <simonpj@microsoft.com> writes: | > | >> Ben, and copying Richard who is far better equipped to respond than | me. | >> | >> I'm way behind the curve here. | >> | >> If "this is precisely what mkFunCo does" why not use mkFunCo? Why do | >> you want to "generalise the arrow operation"? | >> | > Perhaps I should have said "this is what mkFunCo is supposed to do". | > However, mkFunCo needs to be adjusted under the generalized (->) | > scheme, since the (->) tycon will gain two additional type arguments | > (corresponding to the RuntimeReps of the argument and result types). | > mkFunCo needs to fill these type arguments when constructing its | result. | > | >> I'm lost as to your goal and the reason why you need to wade through | this particular swamp. | >> | > There are a few reasons, | > | > * We want to provide a pattern to match against function types | > | > pattern TrFun :: TypeRep arg -> TypeRep res -> TypeRep (arg -> | > res) | > | > * T11120 currently fails on my branch as it contains a TypeRep of a | > promoted type containing an unboxed type. Namely, | > | > import Data.Typeable | > data CharHash = CharHash Char# | > main = print $ typeRep (Proxy :: Proxy 'CharHash) | > | > Note how 'CharHash has kind Char# -> Type. This kind occurs in one of | > the terms in `typeRep` needed in the above program, which currently | > results in core lint failures due to the restrictive kind of (->). | > For this reason (->) needs to be polymorphic over runtime | > representation. | > | > This issue is mentioned in ticket:11714#comment:1. | > | > * I believe there were a few other testcases that failed in similar | > ways to T11120. | > | > For what it's worth, the Type /~ Constraint issue that I'm currently | > fighting with in carrying out the (->) generalization is also the | > cause of another Typeable bug, #11715, so I think this is a worthwhile | > thing to sort out. | > | >> Also your text kind of stops... and then repeats itself. | >> | > Oh dear, I apologize for that. Clipboard malfunction. I've included a | > clean version below for reference. | > | >> We could talk at 2pm UK time tomorrow Weds. Richard would you be | free? | >> | > That would work for me. | > | > Cheers, | > | > - Ben | > | > | > | > | > # Background | > | > Consider what happens when we have the coercions, | > | > co1 :: (a ~ b) | > co2 :: (x ~ y) | > | > where | > | > a :: TYPE ra b :: TYPE rb | > x :: TYPE rx y :: TYPE ry | > | > and we want to construct, | > | > co :: (a -> x) ~ (b -> y) | > | > As I understand it this is precisely what Coercion.mkFunCo does. | > Specifically, co should be a TyConAppCo of (->) applied to co1, co2, | > and coercions showing the equalities ra~rx and rb~ry, | > | > (->) (co_ax :: ra ~ rx) (co_by :: rb ~ ry) co1 co2 | > | > Actually implementing mkFunCo to this specification seems to be not | > too difficult, | > | > -- | Build a function 'Coercion' from two other 'Coercion's. That | is, | > -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) | > ~ (b -> y)@. | > mkFunCo :: Role -> Coercion -> Coercion -> Coercion | > mkFunCo r co1 co2 = | > mkTyConAppCo r funTyCon | > [ mkRuntimeRepCo r co1 -- ra ~ rx where a :: TYPE ra, x :: TYPE | > rx | > , mkRuntimeRepCo r co2 -- rb ~ ry where b :: TYPE rb, y :: TYPE | > ry | > , co1 -- a ~ x | > , co2 -- b ~ y | > ] | > | > -- | For a constraint @co :: (a :: TYPE rep1) ~ (b :: TYPE rep2)@ | > produce | > -- @co' :: rep1 ~ rep2@. | > mkRuntimeRepCo :: Role -> Coercion -> Coercion | > mkRuntimeRepCo r co = mkNthCoRole r 0 $ mkKindCo co | > | Just (tycon, [co]) <- splitTyConAppCo_maybe $ mkKindCo co | > = co | > | otherwise | > = pprPanic "mkRuntimeRepCo: Non-TYPE" (ppr co) | > | > So far, so good (hopefully). | > | > # The Problem | > | > Consider what happens when one of the types is, e.g., HasCallStack. | > For the sake of argument let's say | > | > co1 = <HasCallStack>_R | > co2 = <Int>_R | > | > Recall that HasCallStack is, | > | > type HasCallStack = ((?callStack :: CallStack) :: Constraint) | > | > The problem arises when we attempt to evaluate | > | > mkFunCo r co1 co2 | > | > which will look at the kind coercion of co1, | > | > mkKindCo co1 === <Constraint>_R | > | > and then attempt to splitTyConAppCo it, under the assumption that the | > kind coercion is an application of TYPE, from which we can extract the | > RuntimeRep coercion. Instead we find a nullary TyConAppCo of | > Constraint; things then blow up. | > | > This is the problem. | > | > Ultimately it seems all of this is due to the fact that we play it | > fast- and-loose with Type and Constraint in Core (#11715), especially | > with implicit parameters. I worry that resolving this is more than I | > have time to chew on before 8.2.