This works:
-- Tensor product of two vector spaces
type family Tensor u v :: *
type instance Tensor (Vect k a) (Vect k b) = Vect k (TensorBasis a b)
On Aug 21, 2010, at 9:15 AM, DavidA wrote:
> Brandon S Allbery KF8NH ece.cmu.edu> writes:
>
>>
>>> type Tensor u v =
>>>(u ~ Vect k a, v ~
Brandon S Allbery KF8NH ece.cmu.edu> writes:
>
> > type Tensor u v =
> > (u ~ Vect k a, v ~ Vect k b) => Vect k (TensorBasis a b) -- **
>
> IIRC this actually substitutes as
>
> (forall k a b. (u ~ Vect k a, v ~ Vect k b) => Vect k (TensorBasis a b))
>
> and the implicit forall will gen
