MultConstructor.hs

{-# LANGUAGE GADTSyntax, DataKinds, LinearTypes, KindSignatures, ExplicitForAll #-}
module MultConstructor where

import GHC.Types

data T p a where
  MkT :: a %p -> T p a

{-
this currently fails
g :: forall (b :: Type). T 'Many b %1 -> (b,b)
g (MkT x) = (x,x)
-}