Same question. Do you expect the code below to type-check? I have stripped it
down to essentials. Currently it’s rejected with
Couldn't match type `a' with '(,) k k1 b0 d0
And that seems reasonable, doesn’t it? After all, in the defn of bidStar, (:*)
returns a value of type
Star x y ‘(a,c) ‘(b,d)
which is manifestly incompatible with the claimed, more polymorphic type. And
this is precisely the same error as comes from your class/instance example
below, and for precisely the same reason.
I must be confused.
Simon
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
(:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)
bidStar :: Star T T a a
bidStar = bidT :* bidT
data T a b = MkT
bidT :: T a a
bidT = MkT
From: Edward Kmett [mailto:ekm...@gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional
dependency?
Hrmm. This seems to render product kinds rather useless, as there is no way to
refine the code to reflect the knowledge that they are inhabited by a single
constructor. =(
For instance, there doesn't even seem to be a way to make the following code
compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c -> k a b -> k a c
data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
(:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
instance (Category x, Category y) => Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist example) so
I'm wondering where the impedence mismatch comes in and how to gain knowledge
of this injectivity to make it work.
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
