blob: b3d00069fe073e2957f49220d46c99b2e9c59ca3 (
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 %1 -> ()
elim (U _) = ()
f :: a %1 -> ()
f x = elim (U (\(a :: Void) -> case a of {}))
|
