blob: 03bf8731a7c1be6b30553a863621d94358c5036f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
{-# LANGUAGE GADTs, LinearTypes, ScopedTypeVariables, EmptyCase #-}
module LinearBottomMult where
-- Check that _|_ * Many is not a subusage of One
--
data Void
data U a where U :: a -> U a
elim :: U a #-> ()
elim (U _) = ()
f :: a #-> ()
f x = elim (U (\(a :: Void) -> case a of {}))
|
