PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Edward Kmett]

I've come to think the culprit here is the fallacy that Any should inhabit
every kind.

I realize this is useful from an implementation perspective, but it has a
number of far reaching consequences:

This means that a product kind isn't truly a product of two kinds. x * y,
it winds up as a *distinguishable* x * y + 1, as Andrea has shown us
happens because you can write a type family or MPTC with fundep that can
match on Any.

A coproduct of two kinds x + y, isn't x + y, its x + y + 1.

Kind level naturals aren't kind nats, they are nats + 1, and not even the
one point compactification we get with lazy nats where you have an
indistinguishable infinity added to the domain, but rather there is a
distinguished atom to each kind under consideration.

I noticed that the polykindedness of Any is abused in the GHC.TypeLits to
make fundeps determining a kind, but where else is it exploited?

-Edward

On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> I retract my statement.
>
> My mistake was that I looked at the definition for consistency in FC --
> which correctly is agnostic to non-base-kind coercions -- and applied it
> only to the set of coercion assumptions, not to any coercion derivable from
> the assumptions. As Andrea's example shows, by assuming an eta coercion, it
> is possible to derive an inconsistent coercion.
>
> Examining the definition for FC consistency more closely, an eta coercion
> does not match to the form allowed for coercion assumptions used to prove
> consistency. The proof, in [1], requires all assumptions to have a type
> family application on the left-hand side. An eta coercion does not have a
> type family application on either side, and so the consistency proof in [1]
> does not apply.
>
> In light of this, it would seem that allowing eta coercions while
> retaining consistency would require some more work.
>
> Thanks for pointing out my mistake.
> Richard
>
> [1] S. Weirich et al. "Generative Type Abstraction and Type-level
> Computation."
> (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)
>
> On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:
>
> > On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
> >> [...]
> >> So, it seems possible to introduce eta coercions into FC for all kinds
> containing only one type constructor without sacrificing soundness. How the
> type inference engine/source Haskell triggers the use of these coercions is
> another matter, but there doesn't seem to be anything fundamentally wrong
> with the idea.
> >>
> >
> > A recent snapshot of ghc HEAD doesn't seem to agree:
> >
> > {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> > TypeFamilies, ScopedTypeVariables, TypeOperators #-}
> >
> > import GHC.Exts
> > import Unsafe.Coerce
> >
> > data (:=:) :: k -> k -> * where
> >  Refl :: a :=: a
> >
> > trans :: a :=: b -> b :=: c -> a :=: c
> > trans Refl Refl = Refl
> >
> > type family Fst (x :: (a,b)) :: a
> > type family Snd (x :: (a,b)) :: b
> >
> > type instance Fst '(a,b) = a
> > type instance Snd '(a,b) = b
> >
> > eta :: x :=: '(Fst x, Snd x)
> > eta = unsafeCoerce Refl
> > -- ^^^ this is an acceptable way to simulate new coercions, i hope
> >
> > type family Bad s t  (x :: (a,b)) :: *
> > type instance Bad s t '(a,b) = s
> > type instance Bad s t Any = t
> >
> > refl_Any :: Any :=: Any
> > refl_Any = Refl
> >
> > cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> > cong_Bad Refl = Refl
> >
> > s_eq_t :: forall (s :: *) (t :: *). s :=: t
> > s_eq_t = cong_Bad (trans refl_Any eta)
> >
> > subst :: x :=: y -> x -> y
> > subst Refl x = x
> >
> > coerce :: s -> t
> > coerce = subst s_eq_t
> >
> > {-
> > GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
> > *Main> coerce (4.0 :: Double) :: (Int,Int)
> > (Segmentation fault
> > -}
> >
> > -- Andrea Vezzosi
> >
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120905/565358f9/attachment.htm>