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
| Cc: Simon Peyton Jones
| 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 wrote:
| >
| > Simon Peyton Jones 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.
