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. =(
Wait. When you say “This seems to render produce kinds useless”, are you saying
that in the code I wrote, you think irt should compile?? I reproduce it below
for completeness.
Simon
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Knett where
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
irt :: a x -> Thrist a x
irt ax = ax :- Nil
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
