Linear types (#15981)

This is the first step towards implementation of the linear types proposal
(https://github.com/ghc-proposals/ghc-proposals/pull/111).

It features

* A language extension -XLinearTypes
* Syntax for linear functions in the surface language
* Linearity checking in Core Lint, enabled with -dlinear-core-lint
* Core-to-core passes are mostly compatible with linearity
* Fields in a data type can be linear or unrestricted; linear fields
  have multiplicity-polymorphic constructors.
  If -XLinearTypes is disabled, the GADT syntax defaults to linear fields

The following items are not yet supported:

* a # m -> b syntax (only prefix FUN is supported for now)
* Full multiplicity inference (multiplicities are really only checked)
* Decent linearity error messages
* Linear let, where, and case expressions in the surface language
  (each of these currently introduce the unrestricted variant)
* Multiplicity-parametric fields
* Syntax for annotating lambda-bound or let-bound with a multiplicity
* Syntax for non-linear/multiple-field-multiplicity records
* Linear projections for records with a single linear field
* Linear pattern synonyms
* Multiplicity coercions (test LinearPolyType)

A high-level description can be found at
https://ghc.haskell.org/trac/ghc/wiki/LinearTypes/Implementation
Following the link above you will find a description of the changes made to Core.
This commit has been authored by

* Richard Eisenberg
* Krzysztof Gogolewski
* Matthew Pickering
* Arnaud Spiwack

With contributions from:

* Mark Barbone
* Alexander Vershilov

Updates haddock submodule.

142 files changed, 1637 insertions, 233 deletions

diff --git a/testsuite/tests/callarity/unittest/CallArity1.hs b/testsuite/tests/callarity/unittest/CallArity1.hs
index 60cb97835f..55427ff4b7 100644
--- a/testsuite/tests/callarity/unittest/CallArity1.hs
+++ b/testsuite/tests/callarity/unittest/CallArity1.hs
@@ -1,8 +1,9 @@
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TupleSections, PatternSynonyms #-}
 import GHC.Core
 import GHC.Core.Utils
 import GHC.Types.Id
 import GHC.Core.Type
+import GHC.Core.Multiplicity ( pattern Many )
 import GHC.Core.Make
 import GHC.Core.Opt.CallArity (callArityRHS)
 import GHC.Types.Id.Make
@@ -27,16 +28,16 @@ import GHC.Data.FastString
 go, go2, x, d, n, y, z, scrutf, scruta :: Id
 [go, go2, x,d, n, y, z, scrutf, scruta, f] = mkTestIds
     (words "go go2 x d n y z scrutf scruta f")
-    [ mkVisFunTys [intTy, intTy] intTy
-    , mkVisFunTys [intTy, intTy] intTy
+    [ mkVisFunTysMany [intTy, intTy] intTy
+    , mkVisFunTysMany [intTy, intTy] intTy
     , intTy
-    , mkVisFunTys [intTy] intTy
-    , mkVisFunTys [intTy] intTy
+    , mkVisFunTysMany [intTy] intTy
+    , mkVisFunTysMany [intTy] intTy
     , intTy
     , intTy
-    , mkVisFunTys [boolTy] boolTy
+    , mkVisFunTysMany [boolTy] boolTy
     , boolTy
-    , mkVisFunTys [intTy, intTy] intTy -- protoypical external function
+    , mkVisFunTysMany [intTy, intTy] intTy -- protoypical external function
     ]
 
 exprs :: [(String, CoreExpr)]
@@ -188,7 +189,7 @@ mkLApps v = mkApps (Var v) . map mkLit
 mkACase = mkIfThenElse (mkVarApps (Var scrutf) [scruta])
 
 mkTestId :: Int -> String -> Type -> Id
-mkTestId i s ty = mkSysLocal (mkFastString s) (mkBuiltinUnique i) ty
+mkTestId i s ty = mkSysLocal (mkFastString s) (mkBuiltinUnique i) Many ty
 
 mkTestIds :: [String] -> [Type] -> [Id]
 mkTestIds ns tys = zipWith3 mkTestId [0..] ns tys
diff --git a/testsuite/tests/codeGen/should_compile/T13233.hs b/testsuite/tests/codeGen/should_compile/T13233.hs
new file mode 100644
index 0000000000..bb79856d3b
--- /dev/null
+++ b/testsuite/tests/codeGen/should_compile/T13233.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UnboxedTuples #-}
+module Bug where
+
+import GHC.Exts (TYPE)
+
+class Foo (a :: TYPE rep) where
+  bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+
+baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz = bar (#,#)
diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs
index f24fc03bfb..42a30522f2 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.hs
+++ b/testsuite/tests/codeGen/should_fail/T13233.hs
@@ -3,19 +3,20 @@
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MagicHash #-}
+{-# LANGUAGE LinearTypes #-}
 module Bug where
 
 import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# )
 
 class Foo (a :: TYPE rep) where
-  bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b
+  bar :: forall rep2 (b :: TYPE rep2). (a #-> a #-> b) -> a #-> a #-> b
 
-baz :: forall rep (a :: TYPE rep). Foo a => a -> a -> (# a, a #)
+baz :: forall rep (a :: TYPE rep). Foo a => a #-> a #-> (# a, a #)
 baz = bar (#,#)
 
 obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep)
                    (a :: TYPE rep1) (b :: TYPE rep2).
-                   a -> b -> (# a, b #)) -> ()
+                   a #-> b #-> (# a, b #)) -> ()
 obscure _ = ()
 
 quux :: ()
diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr
index f6254778c1..1bbe161967 100644
--- a/testsuite/tests/codeGen/should_fail/T13233.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233.stderr
@@ -1,27 +1,11 @@
 
-T13233.hs:14:11: error:
-    Cannot use function with levity-polymorphic arguments:
-      (#,#) :: a -> a -> (# a, a #)
-    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
-    are eta-expanded internally because they must occur fully saturated.
-    Use -fprint-typechecker-elaboration to display the full expression.)
-    Levity-polymorphic arguments:
-      a :: TYPE rep
-      a :: TYPE rep
-
-T13233.hs:22:16: error:
-    Cannot use function with levity-polymorphic arguments:
-      (#,#) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}
-                      {a :: TYPE rep1} {b :: TYPE rep2}.
-               a -> b -> (# a, b #)
-    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
-    are eta-expanded internally because they must occur fully saturated.
-    Use -fprint-typechecker-elaboration to display the full expression.)
-    Levity-polymorphic arguments:
-      a :: TYPE rep1
-      b :: TYPE rep2
+T13233.hs:23:16: error:
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE rep1
+    When trying to create a variable of type: a
 
-T13233.hs:27:10: error:
+T13233.hs:28:10: error:
     Cannot use function with levity-polymorphic arguments:
       mkWeak# :: a
                  -> b
diff --git a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
index 40a12ecd62..6a069752f7 100644
--- a/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
+++ b/testsuite/tests/codeGen/should_fail/T13233_elab.stderr
@@ -1,25 +1,11 @@
 
-T13233_elab.hs:17:11: error:
-    Cannot use function with levity-polymorphic arguments:
-      (#,#) @rep @rep @a @a :: a -> a -> (# a, a #)
-    Levity-polymorphic arguments:
-      a :: TYPE rep
-      a :: TYPE rep
-
 T13233_elab.hs:25:16: error:
-    Cannot use function with levity-polymorphic arguments:
-      /\(@(rep1 :: RuntimeRep)).
-      /\(@(rep2 :: RuntimeRep)).
-      /\(@(a :: TYPE rep1)).
-      /\(@(b :: TYPE rep2)).
-      (#,#) @rep1 @rep2 @a @b :: forall {rep1 :: RuntimeRep}
-                                        {rep2 :: RuntimeRep} {a :: TYPE rep1} {b :: TYPE rep2}.
-                                 a -> b -> (# a, b #)
-    Levity-polymorphic arguments:
-      a :: TYPE rep1
-      b :: TYPE rep2
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE rep1
+    When trying to create a variable of type: a
 
-T13233_elab.hs:33:10:
+T13233_elab.hs:33:10: error:
     Cannot use function with levity-polymorphic arguments:
       mkWeak# @rep @a @b @c :: a
                                -> b
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
index 44af3fd5f7..df2f4977f8 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 136724
+  Total ticks: 136962
diff --git a/testsuite/tests/deriving/should_compile/T14682.stderr b/testsuite/tests/deriving/should_compile/T14682.stderr
index 59fc405cdb..2bf9552ff9 100644
--- a/testsuite/tests/deriving/should_compile/T14682.stderr
+++ b/testsuite/tests/deriving/should_compile/T14682.stderr
@@ -21,8 +21,8 @@ Derived class instances:
   
   instance Data.Data.Data T14682.Foo where
     Data.Data.gfoldl k z (T14682.Foo a1 a2)
-      = ((z T14682.Foo `k` a1) `k` a2)
-    Data.Data.gunfold k z _ = k (k (z T14682.Foo))
+      = ((z (\ a1 a2 -> T14682.Foo a1 a2) `k` a1) `k` a2)
+    Data.Data.gunfold k z _ = k (k (z (\ a1 a2 -> T14682.Foo a1 a2)))
     Data.Data.toConstr (T14682.Foo _ _) = T14682.$cFoo
     Data.Data.dataTypeOf _ = T14682.$tFoo
   
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index c83d29b03d..c1c9502863 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -40,6 +40,7 @@ expectedGhcOnlyExtensions =
     [ "RelaxedLayout"
     , "AlternativeLayoutRule"
     , "AlternativeLayoutRuleTransitional"
+    , "LinearTypes"
     ]
 
 expectedCabalOnlyExtensions :: [String]
diff --git a/testsuite/tests/ghci.debugger/scripts/break006.stdout b/testsuite/tests/ghci.debugger/scripts/break006.stdout
index 407ad3739b..2b4a6c20f8 100644
--- a/testsuite/tests/ghci.debugger/scripts/break006.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break006.stdout
@@ -4,14 +4,14 @@ f :: Int -> a = _
 x :: Int = 1
 xs :: [Int] = [2,3]
 xs :: [Int] = [2,3]
-x :: Int = 1
 f :: Int -> a = _
+x :: Int = 1
 _result :: [a] = _
 y = (_t1::a)
 y = 2
 xs :: [Int] = [2,3]
-x :: Int = 1
 f :: Int -> Int = _
+x :: Int = 1
 _result :: [Int] = _
 y :: Int = 2
 _t1 :: Int = 2
diff --git a/testsuite/tests/ghci.debugger/scripts/hist001.stdout b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
index a19a34f315..b52e8aa5fe 100644
--- a/testsuite/tests/ghci.debugger/scripts/hist001.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/hist001.stdout
@@ -20,8 +20,8 @@ _result :: a
 f :: Integer -> a
 x :: Integer
 xs :: [t] = []
-x :: Integer = 2
 f :: Integer -> a = _
+x :: Integer = 2
 _result :: a = _
 _result = 3
 Logged breakpoint at Test3.hs:2:18-31
diff --git a/testsuite/tests/ghci.debugger/scripts/hist002.stdout b/testsuite/tests/ghci.debugger/scripts/hist002.stdout
index a19a34f315..b52e8aa5fe 100644
--- a/testsuite/tests/ghci.debugger/scripts/hist002.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/hist002.stdout
@@ -20,8 +20,8 @@ _result :: a
 f :: Integer -> a
 x :: Integer
 xs :: [t] = []
-x :: Integer = 2
 f :: Integer -> a = _
+x :: Integer = 2
 _result :: a = _
 _result = 3
 Logged breakpoint at Test3.hs:2:18-31
diff --git a/testsuite/tests/ghci/T18060/T18060.stdout b/testsuite/tests/ghci/T18060/T18060.stdout
index 9d6ab23dba..8c3a2794fe 100644
--- a/testsuite/tests/ghci/T18060/T18060.stdout
+++ b/testsuite/tests/ghci/T18060/T18060.stdout
@@ -1,6 +1,6 @@
 type (->) :: * -> * -> *
-data (->) a b
-  	-- Defined in ‘GHC.Prim’
+type (->) = (->) :: * -> * -> *
+  	-- Defined in ‘GHC.Types’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/T8535.stdout b/testsuite/tests/ghci/scripts/T8535.stdout
index 7a949cd465..f7e40fd0f4 100644
--- a/testsuite/tests/ghci/scripts/T8535.stdout
+++ b/testsuite/tests/ghci/scripts/T8535.stdout
@@ -1,6 +1,6 @@
 type (->) :: * -> * -> *
-data (->) a b
-  	-- Defined in ‘GHC.Prim’
+type (->) = (->) :: * -> * -> *
+  	-- Defined in ‘GHC.Types’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/ghci020.stdout b/testsuite/tests/ghci/scripts/ghci020.stdout
index 7a949cd465..f7e40fd0f4 100644
--- a/testsuite/tests/ghci/scripts/ghci020.stdout
+++ b/testsuite/tests/ghci/scripts/ghci020.stdout
@@ -1,6 +1,6 @@
 type (->) :: * -> * -> *
-data (->) a b
-  	-- Defined in ‘GHC.Prim’
+type (->) = (->) :: * -> * -> *
+  	-- Defined in ‘GHC.Types’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/should_run/T10145.stdout b/testsuite/tests/ghci/should_run/T10145.stdout
index 7a949cd465..f7e40fd0f4 100644
--- a/testsuite/tests/ghci/should_run/T10145.stdout
+++ b/testsuite/tests/ghci/should_run/T10145.stdout
@@ -1,6 +1,6 @@
 type (->) :: * -> * -> *
-data (->) a b
-  	-- Defined in ‘GHC.Prim’
+type (->) = (->) :: * -> * -> *
+  	-- Defined in ‘GHC.Types’
 infixr -1 ->
 instance Applicative ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/linear/Makefile b/testsuite/tests/linear/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/linear/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/linear/should_compile/Arity2.hs b/testsuite/tests/linear/should_compile/Arity2.hs
new file mode 100644
index 0000000000..d764d5111a
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Arity2.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module Arity2 where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+-}
+
+--import GHC.Base
+
+data Id a = Id a
+
+(<$>) :: (a -> b) -> Id a -> Id b
+(<$>) f (Id a) = Id (f a)
+
+(<*>) :: Id (a -> b) -> Id a -> Id b
+(<*>) (Id a) (Id b) = Id (a b)
+
+data Q = Q () ()
+data S = S ()
+
+-- Q only gets eta-expand once and then trapped
+foo = Q <$> Id () <*> Id ()
+
+-- This compiles fine
+foo2 = S <$> Id ()
+
+{-
+[1 of 1] Compiling Arity2           ( linear-tests/Arity2.hs, linear-tests/Arity2.o )
+
+linear-tests/Arity2.hs:21:7: error:
+    • Couldn't match type ‘() ⊸ Q’ with ‘() -> b’
+      Expected type: Id (() -> b)
+        Actual type: Id (() ⊸ Q)
+    • In the first argument of ‘(<*>)’, namely ‘Q <$> Id ()’
+      In the expression: Q <$> Id () <*> Id ()
+      In an equation for ‘foo’: foo = Q <$> Id () <*> Id ()
+    • Relevant bindings include
+        foo :: Id b (bound at linear-tests/Arity2.hs:21:1)
+   |
+21 | foo = Q <$> Id () <*> Id ()
+   |       ^^^^^^^^^^^
+-}
diff --git a/testsuite/tests/linear/should_compile/Branches.hs b/testsuite/tests/linear/should_compile/Branches.hs
new file mode 100644
index 0000000000..ee08ade335
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Branches.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE LinearTypes #-}
+module GuardTup where
+
+data Q = Q ()
+
+mkQ :: () -> Q
+mkQ = Q
+
+foo smart
+  | smart = mkQ
+  | otherwise = Q
+
+fooIf smart = if smart then mkQ else Q
diff --git a/testsuite/tests/linear/should_compile/CSETest.hs b/testsuite/tests/linear/should_compile/CSETest.hs
new file mode 100644
index 0000000000..3321dbd43d
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/CSETest.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{- This test makes sure that if two expressions with conflicting types are
+   CSEd then appropiate things happen. -}
+module CSETest where
+
+minimal :: a ⊸ a
+minimal x = x
+
+maximal :: a -> a
+maximal x = x
diff --git a/testsuite/tests/linear/should_compile/Dollar2.hs b/testsuite/tests/linear/should_compile/Dollar2.hs
new file mode 100644
index 0000000000..4cde3dcb45
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Dollar2.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module Dollar2 where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+-}
+
+
+import GHC.Base
+
+data AB = A () | B ()
+
+qux :: Bool
+qux = True
+{-# NOINLINE qux #-}
+
+foo = id $ ((if qux then A else B) $ ())
+
+{-
+
+-}
diff --git a/testsuite/tests/linear/should_compile/DollarDefault.hs b/testsuite/tests/linear/should_compile/DollarDefault.hs
new file mode 100644
index 0000000000..dbe689566a
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/DollarDefault.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes #-}
+module DollarDefault where
+
+class C p where
+  cid :: p a a -> p a a
+
+instance C (->) where
+  cid = id
+
+foo = (cid $ id) $ ()
diff --git a/testsuite/tests/linear/should_compile/DollarTest.hs b/testsuite/tests/linear/should_compile/DollarTest.hs
new file mode 100644
index 0000000000..bc15a4fead
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/DollarTest.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Dollar where
+{-
+Check $ interacting with multiplicity polymorphism.
+This caused Core Lint error previously.
+-}
+
+import GHC.Base
+
+data Q a = Q a
+
+data QU = QU ()
+
+test = QU $ ()
+
+qux = Q $ ()
diff --git a/testsuite/tests/linear/should_compile/Foldr.hs b/testsuite/tests/linear/should_compile/Foldr.hs
new file mode 100644
index 0000000000..759256d5b2
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Foldr.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module FoldrExample where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+-}
+
+import GHC.Base
+import Data.Maybe
+
+qux :: [Maybe Char] -> String
+qux str = foldr (maybe id (:)) "" str
+
+{-
+
+[1 of 1] Compiling FoldrExample     ( linear-tests/Foldr.hs, linear-tests/Foldr.o )
+
+linear-tests/Foldr.hs:11:27: error:
+    • Couldn't match type ‘[Char] ⊸ [Char]’ with ‘[Char] -> [Char]’
+      Expected type: Char -> [Char] -> [Char]
+        Actual type: Char ⊸ [Char] ⊸ [Char]
+    • In the second argument of ‘maybe’, namely ‘(:)’
+      In the first argument of ‘foldr’, namely ‘(maybe id (:))’
+      In the expression: foldr (maybe id (:)) "" str
+   |
+11 | qux str = foldr (maybe id (:)) "" str
+   |                           ^^^
+
+-}
diff --git a/testsuite/tests/linear/should_compile/Iden.hs b/testsuite/tests/linear/should_compile/Iden.hs
new file mode 100644
index 0000000000..3522a43c42
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Iden.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module Foo where
+
+newtype HappyIdentity a = HappyIdentity a
+happyIdentity = HappyIdentity
diff --git a/testsuite/tests/linear/should_compile/Linear10.hs b/testsuite/tests/linear/should_compile/Linear10.hs
new file mode 100644
index 0000000000..e76a344fb0
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear10.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE GADTs #-}
+module Linear10 where
+
+data Unrestricted a where Unrestricted :: a -> Unrestricted a
+
+unrestrictedDup :: Unrestricted a ⊸ (a, a)
+unrestrictedDup (Unrestricted a) = (a,a)
diff --git a/testsuite/tests/linear/should_compile/Linear12.hs b/testsuite/tests/linear/should_compile/Linear12.hs
new file mode 100644
index 0000000000..3f49e94948
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear12.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE GADTs #-}
+module Linear12 where
+
+type N a = a ⊸ ()
+
+consume :: a ⊸ N a ⊸ ()
+consume x k = k x
+
+data N' a where N :: N a ⊸ N' a
+
+consume' :: a ⊸ N' a ⊸ ()
+consume' x (N k) = k x
+
+data W = W (W ⊸ ())
+
+wPlusTwo :: W ⊸ W
+wPlusTwo n = W (\(W k) -> k n)
+
+data Nat = S Nat
+
+natPlusOne :: Nat ⊸ Nat
+natPlusOne n = S n
+
+data D = D ()
+
+mkD :: () ⊸ D
+mkD x = D x
+
+data Odd = E Even
+data Even = O Odd
+
+evenPlusOne :: Even ⊸ Odd
+evenPlusOne e = E e
diff --git a/testsuite/tests/linear/should_compile/Linear14.hs b/testsuite/tests/linear/should_compile/Linear14.hs
new file mode 100644
index 0000000000..3a40212f75
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear14.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear14 where
+
+-- Inference-related behaviour. Slightly sub-optimal still.
+
+bind1 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c
+bind1 b x f = b x (\a -> f a)
+
+newtype I a = I a
+
+bind2 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (I a⊸b) ⊸ c
+bind2 b x f = b x (\a -> f (I a))
+
+bind3 :: (d ⊸ I (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c
+bind3 b x f = b x (I (\a -> f a))
+
+bind4 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
+bind4 b x f = b x (I (\g -> f g))
+
+bind5 :: (d ⊸ ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
+bind5 b x f = b x (\g -> f (\a -> g a))
+
+bind6 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c
+bind6 b x f = b x (I (\g -> f (\a -> g a)))
diff --git a/testsuite/tests/linear/should_compile/Linear15.hs b/testsuite/tests/linear/should_compile/Linear15.hs
new file mode 100644
index 0000000000..fb244fe8b3
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear15.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear15 where
+
+correctWhere :: Int ⊸ Int
+correctWhere a = g a
+  where
+    f :: Int ⊸ Int
+    f x = x
+
+    g :: Int ⊸ Int
+    g x = f x
diff --git a/testsuite/tests/linear/should_compile/Linear16.hs b/testsuite/tests/linear/should_compile/Linear16.hs
new file mode 100644
index 0000000000..8ed8b5b36c
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear16.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE RebindableSyntax #-}
+module Linear16 where
+
+-- Rebindable do notation
+
+(>>=) :: a ⊸ (a ⊸ b) ⊸ b
+(>>=) x f = f x
+
+-- `fail` is needed due to pattern matching on ();
+-- ideally, it shouldn't be there.
+fail :: a
+fail = fail
+
+correctDo = do
+  x <- ()
+  (y,z) <- ((),x)
+  () <- y
+  () <- z
+  ()
diff --git a/testsuite/tests/linear/should_compile/Linear1Rule.hs b/testsuite/tests/linear/should_compile/Linear1Rule.hs
new file mode 100644
index 0000000000..0553c61e84
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear1Rule.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE LinearTypes #-}
+module Linear1Rule where
+
+-- Test the 1 <= p rule
+f :: a #-> b
+f = f
+
+g :: a # p -> b
+g x = f x
diff --git a/testsuite/tests/linear/should_compile/Linear3.hs b/testsuite/tests/linear/should_compile/Linear3.hs
new file mode 100644
index 0000000000..52b9571085
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear3.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear3 where
+
+correctApp1 :: (a⊸b) ⊸ a ⊸ b
+correctApp1 f a = f a
+
+correctApp2 :: (a⊸a) -> a ⊸ a
+correctApp2 f a = f (f a)
+
+correctApp3 :: Int ⊸ Int
+correctApp3 x = f x
+  where
+    f :: Int ⊸ Int
+    f y = y
+
+correctApp4 :: Int ⊸ Int
+correctApp4 x = f (f x)
+  where
+    f :: Int ⊸ Int
+    f y = y
+
+correctIf :: Bool ⊸ a ⊸ a
+correctIf x n =
+   if x then n else n
diff --git a/testsuite/tests/linear/should_compile/Linear4.hs b/testsuite/tests/linear/should_compile/Linear4.hs
new file mode 100644
index 0000000000..7f025e0a0f
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear4.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LambdaCase, GADTs #-}
+module Linear4 where
+
+correctCase :: Bool ⊸ a ⊸ a
+correctCase x n =
+  case x of
+    True -> n
+    False -> n
diff --git a/testsuite/tests/linear/should_compile/Linear6.hs b/testsuite/tests/linear/should_compile/Linear6.hs
new file mode 100644
index 0000000000..ea095237f5
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear6.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear6 where
+
+correctEqn :: Bool ⊸ Int ⊸ Int
+correctEqn True  n = n
+correctEqn False n = n
diff --git a/testsuite/tests/linear/should_compile/Linear8.hs b/testsuite/tests/linear/should_compile/Linear8.hs
new file mode 100644
index 0000000000..a7b6bf95e0
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Linear8.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LambdaCase #-}
+module Linear8 where
+
+correctLCase :: Int ⊸ Bool -> Int
+correctLCase n = \case
+  True -> n
+  False -> n
diff --git a/testsuite/tests/linear/should_compile/LinearConstructors.hs b/testsuite/tests/linear/should_compile/LinearConstructors.hs
new file mode 100644
index 0000000000..0e0f1b547e
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearConstructors.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TupleSections #-}
+module LinearConstructors where
+
+data T a b = MkT a b
+
+f1 :: a #-> b #-> T a b
+f1 = MkT
+
+f2 :: a #-> b -> T a b
+f2 = MkT
+
+f3 :: a -> b #-> T a b
+f3 = MkT
+
+f4 :: a -> b -> T a b
+f4 = MkT
+
+-- tuple sections
+g1 :: a #-> b #-> (a, b, Int)
+g1 = (,,0)
+
+g2 :: a #-> b -> (a, b, Int)
+g2 = (,,0)
+
+g3 :: a -> b #-> (a, b, Int)
+g3 = (,,0)
+
+g4 :: a -> b -> (a, b, Int)
+g4 = (,,0)
diff --git a/testsuite/tests/linear/should_compile/LinearEmptyCase.hs b/testsuite/tests/linear/should_compile/LinearEmptyCase.hs
new file mode 100644
index 0000000000..daa1918b56
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearEmptyCase.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE EmptyCase, LinearTypes #-}
+
+module LinearEmptyCase where
+
+data Void
+
+f :: a #-> Void -> b
+f x y = case y of {}
diff --git a/testsuite/tests/linear/should_compile/LinearGuards.hs b/testsuite/tests/linear/should_compile/LinearGuards.hs
new file mode 100644
index 0000000000..fae1208176
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearGuards.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearGuards where
+
+f :: Bool -> a #-> a
+f b a | b = a
+      | True = a
diff --git a/testsuite/tests/linear/should_compile/LinearLetRec.hs b/testsuite/tests/linear/should_compile/LinearLetRec.hs
new file mode 100644
index 0000000000..e7cf71d324
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearLetRec.hs
@@ -0,0 +1,11 @@
+module NameCache where
+
+data Name = Name
+data NameCache = NameCache !Int !Name
+
+extendOrigNameCache :: Name -> Name -> Name
+extendOrigNameCache _ _ = Name
+
+initNameCache :: Int -> [Name] -> NameCache
+initNameCache us names
+  = NameCache us (foldl extendOrigNameCache Name names)
diff --git a/testsuite/tests/linear/should_compile/LinearPolyDollar.hs b/testsuite/tests/linear/should_compile/LinearPolyDollar.hs
new file mode 100644
index 0000000000..7d14351cfc
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearPolyDollar.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearPolyDollar where
+
+-- The goal of this test is to ensure that the special typing rule of ($) plays
+-- well with multiplicity-polymorphic functions
+
+data F = F Bool
+
+x = F $ True
diff --git a/testsuite/tests/linear/should_compile/LinearTH1.hs b/testsuite/tests/linear/should_compile/LinearTH1.hs
new file mode 100644
index 0000000000..4f19b3b449
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearTH1.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes, TemplateHaskell #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module LinearTH1 where
+
+x1 = [t|Int -> Int|]
diff --git a/testsuite/tests/linear/should_compile/LinearTH2.hs b/testsuite/tests/linear/should_compile/LinearTH2.hs
new file mode 100644
index 0000000000..a35f9a1c7e
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearTH2.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE LinearTypes, TemplateHaskell, RankNTypes #-}
+module LinearTH2 where
+
+x1 = [t|forall p. Int # p -> Int|]
diff --git a/testsuite/tests/linear/should_compile/List.hs b/testsuite/tests/linear/should_compile/List.hs
new file mode 100644
index 0000000000..4d87dba896
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/List.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module List where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+
+See Cabal:Distribution.Types.VersionRange:556
+-}
+
+import GHC.Base
+
+data J = J ()
+
+j :: () -> J
+j = J
+
+tup = (j, J)
+tup2 = (J, j)
+
+tup3 = [j, J]
+tup4 = [J, j]
+
+{-
+
+[1 of 1] Compiling List             ( linear-tests/List.hs, linear-tests/List.o )
+
+linear-tests/List.hs:17:12: error:
+    • Couldn't match expected type ‘() -> J’ with actual type ‘() ⊸ J’
+    • In the expression: J
+      In the expression: [j, J]
+      In an equation for ‘tup3’: tup3 = [j, J]
+   |
+17 | tup3 = [j, J]
+   |            ^
+
+linear-tests/List.hs:18:12: error:
+    • Couldn't match expected type ‘() ⊸ J’ with actual type ‘() -> J’
+    • In the expression: j
+      In the expression: [J, j]
+      In an equation for ‘tup4’: tup4 = [J, j]
+   |
+18 | tup4 = [J, j]
+   |            ^
+
+-}
diff --git a/testsuite/tests/linear/should_compile/Makefile b/testsuite/tests/linear/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/linear/should_compile/MultConstructor.hs b/testsuite/tests/linear/should_compile/MultConstructor.hs
new file mode 100644
index 0000000000..6e631774ba
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/MultConstructor.hs
@@ -0,0 +1,13 @@
+{-# 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 #-> (b,b)
+g (MkT x) = (x,x)
+-}
diff --git a/testsuite/tests/linear/should_compile/OldList.hs b/testsuite/tests/linear/should_compile/OldList.hs
new file mode 100644
index 0000000000..2ed7b8aaf2
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/OldList.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude, ScopedTypeVariables, BangPatterns, RankNTypes #-}
+
+{-
+This is a simplified version of Data.OldList module from base.
+This caused an assertion failure in earlier version of linear
+types implementation.
+-}
+
+module Data.OldList where
+
+import GHC.Base
+
+sortBy :: forall a . (a -> a -> Ordering) -> [a]
+sortBy cmp = []
+  where
+    sequences (a:b:xs)
+      | a `cmp` b == GT = descending b [a]  xs
+      | otherwise       = ascending  b (a:) xs
+    sequences xs = [xs]
+
+--    descending :: a -> [a] -> [a] -> [[a]]
+    descending a as (b:bs)
+      | a `cmp` b == GT = descending b (a:as) bs
+    descending a as bs  = (a:as): sequences bs
+
+    ascending :: a -> (forall i . [a] # i -> [a]) -> [a] -> [[a]]
+    ascending a as (b:bs)
+      | a `cmp` b /= GT = ascending b foo bs
+      where
+        foo :: [a] # k -> [a]
+        foo ys = as (a:ys)
+    ascending a as bs   = let !x = as [a]
+                          in x : sequences bs
diff --git a/testsuite/tests/linear/should_compile/Op.hs b/testsuite/tests/linear/should_compile/Op.hs
new file mode 100644
index 0000000000..725fd222d9
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Op.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+module Op where
+{-
+See Control.Arrow and Data.Functor.Contravariant
+-}
+
+import GHC.Base
+
+class Or p where
+    or :: p a b -> p a b -> p a b
+
+instance Or (->) where
+    or x _ = x
+
+
+foo = or Just (\x -> Just x)
+
+{-
+This caused an error in the earlier version of linear types:
+
+linear-tests/Op.hs:18:16: error:
+    • Couldn't match expected type ‘a ⊸ Maybe a’
+                  with actual type ‘a0 -> Maybe a0’
+    • The lambda expression ‘\ x -> Just x’ has one argument,
+      its type is ‘p0 a b0’,
+      it is specialized to ‘a ⊸ Maybe a’
+      In the second argument of ‘or’, namely ‘(\ x -> Just x)’
+      In the expression: or Just (\ x -> Just x)
+    • Relevant bindings include
+        foo :: a ⊸ Maybe a (bound at linear-tests/Op.hs:18:1)
+   |
+18 | foo = or Just (\x -> Just x)
+   |                ^^^^^^^^^^^^
+-}
diff --git a/testsuite/tests/linear/should_compile/Pr110.hs b/testsuite/tests/linear/should_compile/Pr110.hs
new file mode 100644
index 0000000000..a3311cb7b8
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Pr110.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes #-}
+module Pr110 where
+
+data Bloop = Bloop Bool
+
+g :: Bloop #-> Bool
+g (Bloop x) = x
+
+h :: Bool #-> Bloop
+h x = Bloop x
diff --git a/testsuite/tests/linear/should_compile/RankN.hs b/testsuite/tests/linear/should_compile/RankN.hs
new file mode 100644
index 0000000000..cadefa5290
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/RankN.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RankNTypes #-}
+module RankN where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+-}
+
+import GHC.Base
+{-
+class Data a where
+  gunfold :: (forall b r.  c (b -> r) -> c r)
+          -> (forall r. r -> c r)
+          -> c a
+
+foo = 1
+{-# NOINLINE foo #-}
+
+instance Data [a] where
+  gunfold k z = k (k (z (:)))
+
+
+--qux :: Identity (Int ⊸ Int)
+qux = Identity Just
+
+app :: Identity (a -> b) -> Identity a -> Identity b
+app (Identity f) (Identity a) = Identity (f a)
+
+example = app qux (Identity 5)
+
+--unqux :: Int ⊸ Int
+unqux = Just
+
+unapp :: (a -> b) -> a -> b
+unapp f a = f a
+
+example1 = unapp unqux 5
+
+foo :: Identity (a -> b) -> a -> b
+foo = runIdentity
+
+fooTest = foo (Identity Just)
+
+foo2 :: (a -> b) -> a -> b
+foo2 = ($)
+
+fooTest2 = let f = Just in foo2 f
+-}
+
+data Identity a = Identity { runIdentity :: a }
+
+extraTest = (id Identity) :: a -> Identity a
diff --git a/testsuite/tests/linear/should_compile/T1735Min.hs b/testsuite/tests/linear/should_compile/T1735Min.hs
new file mode 100644
index 0000000000..8800272328
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/T1735Min.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UndecidableInstances, Rank2Types,
+    KindSignatures, EmptyDataDecls, MultiParamTypeClasses, CPP #-}
+
+module T1735_Help.Basics where
+
+data Proxy a = Proxy
+
+class Data ctx a where
+     gunfold :: Proxy ctx
+             -> (forall b r. Data ctx b => c (b -> r) -> c r)
+             -> (forall r. r -> c r)
+             -> Constr
+             -> c a
+
+
+newtype ID x = ID { unID :: x }
+
+fromConstrB :: Data ctx a
+            => Proxy ctx
+            -> (forall b. Data ctx b => b)
+            -> Constr
+            -> a
+fromConstrB ctx f = unID . gunfold ctx k z
+ where
+  k c = ID (unID c f)
+  z = ID
+
+data Constr = Constr
diff --git a/testsuite/tests/linear/should_compile/Tunboxer.hs b/testsuite/tests/linear/should_compile/Tunboxer.hs
new file mode 100644
index 0000000000..c6bc7f5f38
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/Tunboxer.hs
@@ -0,0 +1,11 @@
+{-# OPTIONS_GHC -O #-}
+module TUnboxer where
+
+-- This checks that the multiplicity of unboxer inside MkId.wrapCo is correct.
+-- The test is a minimized version of base/GHC/Event/PSQ.hs and requires -O.
+newtype Unique = Unique Int
+
+data IntPSQ = Bin !Unique
+
+deleteView :: Unique -> ()
+deleteView k = Bin k `seq` ()
diff --git a/testsuite/tests/linear/should_compile/TupSection.hs b/testsuite/tests/linear/should_compile/TupSection.hs
new file mode 100644
index 0000000000..ea401e6e97
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/TupSection.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE TupleSections #-}
+module TupSection where
+{-
+inplace/bin/ghc-stage1 -O2 -dcore-lint
+-}
+
+myAp :: (a -> b) -> a -> b
+myAp f x = f x
+
+foo = myAp (,()) ()
+
+qux = ("go2",) $ ()
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
new file mode 100644
index 0000000000..8b11b9ccb9
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -0,0 +1,37 @@
+broken_multiplicity_syntax = 94  # https://github.com/tweag/ghc/issues/94
+
+test('anf', normal, compile, [''])
+test('Arity2', normal, compile, [''])
+test('Branches', normal, compile, [''])
+test('CSETest', normal, compile, [''])
+test('Dollar2', normal, compile, [''])
+test('DollarDefault', normal, compile, [''])
+test('DollarTest', normal, compile, [''])
+test('Foldr', normal, compile, [''])
+test('Iden', normal, compile, [''])
+test('List', normal, compile, [''])
+test('OldList', expect_broken(broken_multiplicity_syntax), compile, [''])
+test('Op', normal, compile, [''])
+test('RankN', normal, compile, [''])
+test('T1735Min', normal, compile, [''])
+test('TupSection', normal, compile, [''])
+test('Pr110', normal, compile, [''])
+test('Linear10', normal, compile, [''])
+test('Linear12', normal, compile, [''])
+test('Linear14', expect_broken(298), compile, [''])
+test('Linear15', normal, compile, [''])
+test('Linear16', normal, compile, [''])
+test('Linear3', normal, compile, [''])
+test('Linear4', expect_broken(20), compile, [''])
+test('Linear6', normal, compile, [''])
+test('Linear8', normal, compile, [''])
+test('LinearGuards', normal, compile, [''])
+test('LinearPolyDollar', normal, compile, [''])
+test('LinearConstructors', normal, compile, [''])
+test('Linear1Rule', expect_broken(broken_multiplicity_syntax), compile, [''])
+test('LinearEmptyCase', normal, compile, [''])
+test('Tunboxer', normal, compile, [''])
+test('MultConstructor', expect_broken(broken_multiplicity_syntax), compile, [''])
+test('LinearLetRec', expect_broken(405), compile, ['-O -dlinear-core-lint'])
+test('LinearTH1', normal, compile, [''])
+test('LinearTH2', expect_broken(broken_multiplicity_syntax), compile, [''])
diff --git a/testsuite/tests/linear/should_compile/anf.hs b/testsuite/tests/linear/should_compile/anf.hs
new file mode 100644
index 0000000000..9f1982e397
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/anf.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE LinearTypes #-}
+-- !! Data constructors with strict fields
+-- This test should use -funbox-strict-fields
+
+module Main ( main ) where
+
+main = print (g (f t))
+
+t = MkT 1 2 (3,4) (MkS 5 6)
+
+g (MkT x _ _ _) = x
+
+data T = MkT Int !Int !(Int,Int) !(S Int)
+
+data S a = MkS a a
+
+
+{-# NOINLINE f #-}
+f :: T -> T     -- Takes apart the thing and puts it
+                -- back together differently
+f (MkT x y (a,b) (MkS p q)) = MkT a b (p,q) (MkS x y)
diff --git a/testsuite/tests/linear/should_fail/Linear1.hs b/testsuite/tests/linear/should_fail/Linear1.hs
new file mode 100644
index 0000000000..cdb7eed939
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear1.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LambdaCase, GADTs #-}
+{-# LANGUAGE RebindableSyntax #-}
+module Linear1 where
+
+
+-- Must fail:
+incorrectDup :: a ⊸ (a,a)
+incorrectDup x = (x,x)
+
+-- Must fail:
+incorrectDrop :: a ⊸ ()
+incorrectDrop x = ()
diff --git a/testsuite/tests/linear/should_fail/Linear1.stderr b/testsuite/tests/linear/should_fail/Linear1.stderr
new file mode 100644
index 0000000000..c549d75be3
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear1.stderr
@@ -0,0 +1,10 @@
+
+Linear1.hs:10:14: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectDup’: incorrectDup x = (x, x)
+
+Linear1.hs:14:15: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectDrop’: incorrectDrop x = ()
diff --git a/testsuite/tests/linear/should_fail/Linear11.hs b/testsuite/tests/linear/should_fail/Linear11.hs
new file mode 100644
index 0000000000..67b930ac57
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear11.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear11 where
+
+data Unrestricted a where Unrestricted :: a -> Unrestricted a
+
+incorrectUnrestricted :: a ⊸ Unrestricted a
+incorrectUnrestricted a = Unrestricted a
+
+data NotUnrestricted a where NotUnrestricted :: a ⊸ NotUnrestricted a
+
+incorrectUnrestrictedDup :: NotUnrestricted a ⊸ (a,a)
+incorrectUnrestrictedDup (NotUnrestricted a) = (a,a)
diff --git a/testsuite/tests/linear/should_fail/Linear11.stderr b/testsuite/tests/linear/should_fail/Linear11.stderr
new file mode 100644
index 0000000000..cb52fa16f4
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear11.stderr
@@ -0,0 +1,13 @@
+
+Linear11.hs:9:23: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘a’
+    • In an equation for ‘incorrectUnrestricted’:
+          incorrectUnrestricted a = Unrestricted a
+
+Linear11.hs:14:43: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘a’
+    • In the pattern: NotUnrestricted a
+      In an equation for ‘incorrectUnrestrictedDup’:
+          incorrectUnrestrictedDup (NotUnrestricted a) = (a, a)
diff --git a/testsuite/tests/linear/should_fail/Linear13.hs b/testsuite/tests/linear/should_fail/Linear13.hs
new file mode 100644
index 0000000000..7b9e09c52b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear13.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear13 where
+
+incorrectLet :: a ⊸ ()
+incorrectLet a = let x = a in ()
+
+incorrectLetWithSignature :: (Bool->Bool) #-> ()
+incorrectLetWithSignature x = let y :: Bool->Bool; y = x in ()
+
+incorrectLazyMatch :: (a,b) ⊸ b
+incorrectLazyMatch x = let (a,b) = x in b
+
+incorrectCasePromotion :: (a,b) ⊸ b
+incorrectCasePromotion x = case x of (a,b) -> b
diff --git a/testsuite/tests/linear/should_fail/Linear13.stderr b/testsuite/tests/linear/should_fail/Linear13.stderr
new file mode 100644
index 0000000000..a781c20da6
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear13.stderr
@@ -0,0 +1,28 @@
+
+Linear13.hs:6:14: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘a’
+    • In an equation for ‘incorrectLet’:
+          incorrectLet a = let x = a in ()
+
+Linear13.hs:9:27: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectLetWithSignature’:
+          incorrectLetWithSignature x
+            = let
+                y :: Bool -> Bool
+                y = x
+              in ()
+
+Linear13.hs:12:20: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectLazyMatch’:
+          incorrectLazyMatch x = let (a, b) = x in b
+
+Linear13.hs:15:24: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectCasePromotion’:
+          incorrectCasePromotion x = case x of { (a, b) -> b }
diff --git a/testsuite/tests/linear/should_fail/Linear17.hs b/testsuite/tests/linear/should_fail/Linear17.hs
new file mode 100644
index 0000000000..1d8abfdb09
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear17.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE RebindableSyntax #-}
+module Linear17 where
+
+-- Rebindable do notation
+
+(>>=) :: a ⊸ (a ⊸ b) ⊸ b
+(>>=) x f = f x
+
+-- `fail` is needed due to pattern matching on ();
+-- ideally, it shouldn't be there.
+fail :: a
+fail = fail
+
+incorrectDo1 = do
+  x <- ()
+  (y,z) <- ((),())
+  () <- y
+  () <- z
+  ()
+
+incorrectDo2 = do
+  x <- ()
+  (y,z) <- ((),x)
+  () <- y
+  ()
+
+incorrectDo3 = do
+  x <- ()
+  (y,z) <- (x,x)
+  () <- y
+  () <- z
+  ()
diff --git a/testsuite/tests/linear/should_fail/Linear17.stderr b/testsuite/tests/linear/should_fail/Linear17.stderr
new file mode 100644
index 0000000000..12193e115b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear17.stderr
@@ -0,0 +1,45 @@
+
+Linear17.hs:17:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In a stmt of a 'do' block: x <- ()
+      In the expression:
+        do x <- ()
+           (y, z) <- ((), ())
+           () <- y
+           () <- z
+           ....
+      In an equation for ‘incorrectDo1’:
+          incorrectDo1
+            = do x <- ()
+                 (y, z) <- ((), ())
+                 () <- y
+                 ....
+
+Linear17.hs:25:6: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘z’
+    • In the pattern: (y, z)
+      In a stmt of a 'do' block: (y, z) <- ((), x)
+      In the expression:
+        do x <- ()
+           (y, z) <- ((), x)
+           () <- y
+           ()
+
+Linear17.hs:30:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In a stmt of a 'do' block: x <- ()
+      In the expression:
+        do x <- ()
+           (y, z) <- (x, x)
+           () <- y
+           () <- z
+           ....
+      In an equation for ‘incorrectDo3’:
+          incorrectDo3
+            = do x <- ()
+                 (y, z) <- (x, x)
+                 () <- y
+                 ....
diff --git a/testsuite/tests/linear/should_fail/Linear2.hs b/testsuite/tests/linear/should_fail/Linear2.hs
new file mode 100644
index 0000000000..bb6f525f01
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear2.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear2 where
+
+dup :: a -> (a,a)
+dup x = (x,x)
+
+incorrectApp1 :: a ⊸ ((a,Int),(a,Int))
+incorrectApp1 x = dup (x,0)
+
+incorrectApp2 :: (a->b) -> a ⊸ b
+incorrectApp2 f x = f x
+
+incorrectIf :: Bool -> Int ⊸ Int
+incorrectIf x n =
+  if x then n else 0
diff --git a/testsuite/tests/linear/should_fail/Linear2.stderr b/testsuite/tests/linear/should_fail/Linear2.stderr
new file mode 100644
index 0000000000..eec52922a0
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear2.stderr
@@ -0,0 +1,16 @@
+
+Linear2.hs:9:15: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectApp1’: incorrectApp1 x = dup (x, 0)
+
+Linear2.hs:12:17: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘incorrectApp2’: incorrectApp2 f x = f x
+
+Linear2.hs:15:15: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘n’
+    • In an equation for ‘incorrectIf’:
+          incorrectIf x n = if x then n else 0
diff --git a/testsuite/tests/linear/should_fail/Linear5.hs b/testsuite/tests/linear/should_fail/Linear5.hs
new file mode 100644
index 0000000000..ad0c80356c
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear5.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear5 where
+
+incorrectEqn :: Bool -> Int ⊸ Int
+incorrectEqn True  n = n
+incorrectEqn False n = 0
diff --git a/testsuite/tests/linear/should_fail/Linear5.stderr b/testsuite/tests/linear/should_fail/Linear5.stderr
new file mode 100644
index 0000000000..4de49fb9d9
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear5.stderr
@@ -0,0 +1,5 @@
+
+Linear5.hs:7:20: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘n’
+    • In an equation for ‘incorrectEqn’: incorrectEqn False n = 0
diff --git a/testsuite/tests/linear/should_fail/Linear7.hs b/testsuite/tests/linear/should_fail/Linear7.hs
new file mode 100644
index 0000000000..9ee6438b11
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear7.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LambdaCase #-}
+module Linear7 where
+
+incorrectLCase :: Int ⊸ Bool -> Int
+incorrectLCase n = \case
+  True -> n
+  False -> 0
diff --git a/testsuite/tests/linear/should_fail/Linear7.stderr b/testsuite/tests/linear/should_fail/Linear7.stderr
new file mode 100644
index 0000000000..9dc596477d
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear7.stderr
@@ -0,0 +1,9 @@
+
+Linear7.hs:7:16: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘n’
+    • In an equation for ‘incorrectLCase’:
+          incorrectLCase n
+            = \case
+                True -> n
+                False -> 0
diff --git a/testsuite/tests/linear/should_fail/Linear9.hs b/testsuite/tests/linear/should_fail/Linear9.hs
new file mode 100644
index 0000000000..011c58e837
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear9.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnicodeSyntax #-}
+module Linear9 where
+
+fst :: (a,b) -> a
+fst (a,_) = a
+
+incorrectFst :: (a,b) ⊸ a
+incorrectFst (a,_) = a
+
+incorrectFstVar :: (a,b) ⊸ a
+incorrectFstVar (a,b) = a
+
+incorrectFirstDup :: (a,b) ⊸ ((a,a),b)
+incorrectFirstDup (a,b) = ((a,a),b)
+
+incorrectFstFst :: ((a,b),c) ⊸ a
+incorrectFstFst ((a,_),_) = a
+
+data Test a
+  = Foo a a
+  | Bar a
+
+incorrectTestFst :: Test a ⊸ a
+incorrectTestFst (Foo a _) = a
+incorrectTestFst (Bar a)   = a
diff --git a/testsuite/tests/linear/should_fail/Linear9.stderr b/testsuite/tests/linear/should_fail/Linear9.stderr
new file mode 100644
index 0000000000..ab13270ee3
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Linear9.stderr
@@ -0,0 +1,43 @@
+
+Linear9.hs:9:17: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: _
+      In the pattern: (a, _)
+      In an equation for ‘incorrectFst’: incorrectFst (a, _) = a
+
+Linear9.hs:12:20: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘b’
+    • In the pattern: (a, b)
+      In an equation for ‘incorrectFstVar’: incorrectFstVar (a, b) = a
+
+Linear9.hs:15:20: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘a’
+    • In the pattern: (a, b)
+      In an equation for ‘incorrectFirstDup’:
+          incorrectFirstDup (a, b) = ((a, a), b)
+
+Linear9.hs:18:21: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: _
+      In the pattern: (a, _)
+      In the pattern: ((a, _), _)
+
+Linear9.hs:18:24: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: _
+      In the pattern: ((a, _), _)
+      In an equation for ‘incorrectFstFst’:
+          incorrectFstFst ((a, _), _) = a
+
+Linear9.hs:25:25: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: _
+      In the pattern: Foo a _
+      In an equation for ‘incorrectTestFst’:
+          incorrectTestFst (Foo a _) = a
diff --git a/testsuite/tests/linear/should_fail/LinearAsPat.hs b/testsuite/tests/linear/should_fail/LinearAsPat.hs
new file mode 100644
index 0000000000..e756f4369f
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearAsPat.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearAsPat where
+
+shouldFail :: Bool #-> Bool
+shouldFail x@True = x
diff --git a/testsuite/tests/linear/should_fail/LinearAsPat.stderr b/testsuite/tests/linear/should_fail/LinearAsPat.stderr
new file mode 100644
index 0000000000..7d6cc245cf
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearAsPat.stderr
@@ -0,0 +1,5 @@
+
+LinearAsPat.hs:6:12: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In an equation for ‘shouldFail’: shouldFail x@True = x
diff --git a/testsuite/tests/linear/should_fail/LinearBottomMult.hs b/testsuite/tests/linear/should_fail/LinearBottomMult.hs
new file mode 100644
index 0000000000..03bf8731a7
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearBottomMult.hs
@@ -0,0 +1,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 {}))
diff --git a/testsuite/tests/linear/should_fail/LinearBottomMult.stderr b/testsuite/tests/linear/should_fail/LinearBottomMult.stderr
new file mode 100644
index 0000000000..fd846070d8
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearBottomMult.stderr
@@ -0,0 +1,6 @@
+
+LinearBottomMult.hs:13:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f’:
+          f x = elim (U (\ (a :: Void) -> case a of))
diff --git a/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs b/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs
new file mode 100644
index 0000000000..2cd1628eeb
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearConfusedDollar where
+
+-- When ($) becomes polymorphic in the multiplicity, then, this test case won't
+-- hold anymore. But, as it stands, it produces untyped desugared code, hence
+-- must be rejected.
+
+f :: a #-> a
+f x = x
+
+g :: a #-> a
+g x = f $ x
diff --git a/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr
new file mode 100644
index 0000000000..4abdd1c18c
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr
@@ -0,0 +1,6 @@
+
+LinearConfusedDollar.hs:12:7: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from an application
+    • In the expression: f $ x
+      In an equation for ‘g’: g x = f $ x
diff --git a/testsuite/tests/linear/should_fail/LinearErrOrigin.hs b/testsuite/tests/linear/should_fail/LinearErrOrigin.hs
new file mode 100644
index 0000000000..1eeb149959
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearErrOrigin.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearErrOrigin where
+
+-- The error message should mention "arising from multiplicity of x".
+
+foo :: (a # p -> b) -> a # q -> b
+foo f x = f x
diff --git a/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr b/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
new file mode 100644
index 0000000000..10b889a9a8
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr
@@ -0,0 +1,16 @@
+
+LinearErrOrigin.hs:7:7: error:
+    • Couldn't match type ‘p’ with ‘q’ arising from multiplicity of ‘x’
+      ‘p’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b. (a -> b) -> a -> b
+        at LinearErrOrigin.hs:6:1-35
+      ‘q’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b. (a -> b) -> a -> b
+        at LinearErrOrigin.hs:6:1-35
+    • In an equation for ‘foo’: foo f x = f x
+    • Relevant bindings include
+        f :: a # p -> b (bound at LinearErrOrigin.hs:7:5)
+        foo :: (a # p -> b) -> a # q -> b
+          (bound at LinearErrOrigin.hs:7:1)
diff --git a/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs b/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs
new file mode 100644
index 0000000000..789b8cc3b6
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs
@@ -0,0 +1,3 @@
+{-# LANGUAGE LinearTypes, GADTs #-}
+newtype A where
+   A :: Int -> A
diff --git a/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr b/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
new file mode 100644
index 0000000000..42207d4f72
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
@@ -0,0 +1,5 @@
+
+LinearGADTNewtype.hs:3:4: error:
+    • A newtype constructor must be linear
+    • In the definition of data constructor ‘A’
+      In the newtype declaration for ‘A’
diff --git a/testsuite/tests/linear/should_fail/LinearIf.hs b/testsuite/tests/linear/should_fail/LinearIf.hs
new file mode 100644
index 0000000000..b19873120c
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearIf.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module LinearIf where
+
+import Prelude (Bool(..), Char)
+
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True x _ = x
+ifThenElse False _ y = y
+
+f :: Bool #-> Char #-> Char #-> Char
+f b x y = if b then x else y
+  -- 'f' ought to be unrestricted in all three arguments because it desugars to
+  -- > ifThenElse b x y
diff --git a/testsuite/tests/linear/should_fail/LinearIf.stderr b/testsuite/tests/linear/should_fail/LinearIf.stderr
new file mode 100644
index 0000000000..c34bec5f4d
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearIf.stderr
@@ -0,0 +1,15 @@
+
+LinearIf.hs:13:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘b’
+    • In an equation for ‘f’: f b x y = if b then x else y
+
+LinearIf.hs:13:5: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f’: f b x y = if b then x else y
+
+LinearIf.hs:13:7: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘y’
+    • In an equation for ‘f’: f b x y = if b then x else y
diff --git a/testsuite/tests/linear/should_fail/LinearKind.hs b/testsuite/tests/linear/should_fail/LinearKind.hs
new file mode 100644
index 0000000000..a60554a7a7
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE LinearTypes, KindSignatures #-}
+module LinearKind where
+
+data A :: * #-> *
diff --git a/testsuite/tests/linear/should_fail/LinearKind.stderr b/testsuite/tests/linear/should_fail/LinearKind.stderr
new file mode 100644
index 0000000000..5ac2825b21
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind.stderr
@@ -0,0 +1,5 @@
+
+LinearKind.hs:4:11: error:
+    • Linear arrows disallowed in kinds: * #-> *
+    • In the kind ‘* #-> *’
+      In the data type declaration for ‘A’
diff --git a/testsuite/tests/linear/should_fail/LinearLazyPat.hs b/testsuite/tests/linear/should_fail/LinearLazyPat.hs
new file mode 100644
index 0000000000..8ed4024c40
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLazyPat.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLazyPat where
+
+f :: (a,b) #-> (b,a)
+f ~(x,y) = (y,x)
diff --git a/testsuite/tests/linear/should_fail/LinearLazyPat.stderr b/testsuite/tests/linear/should_fail/LinearLazyPat.stderr
new file mode 100644
index 0000000000..1893d10417
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLazyPat.stderr
@@ -0,0 +1,6 @@
+
+LinearLazyPat.hs:5:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: ~(x, y)
+      In an equation for ‘f’: f ~(x, y) = (y, x)
diff --git a/testsuite/tests/linear/should_fail/LinearLet.hs b/testsuite/tests/linear/should_fail/LinearLet.hs
new file mode 100644
index 0000000000..bf822a8a6e
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet where
+
+f :: a #-> (a,a)
+f x = let y = x in (y,y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet.stderr b/testsuite/tests/linear/should_fail/LinearLet.stderr
new file mode 100644
index 0000000000..3b94833d7e
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet.stderr
@@ -0,0 +1,5 @@
+
+LinearLet.hs:5:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f’: f x = let y = x in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearNoExt.hs b/testsuite/tests/linear/should_fail/LinearNoExt.hs
new file mode 100644
index 0000000000..2671246f21
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearNoExt.hs
@@ -0,0 +1,3 @@
+module LinearNoExt where
+
+type T = a #-> a
diff --git a/testsuite/tests/linear/should_fail/LinearNoExt.stderr b/testsuite/tests/linear/should_fail/LinearNoExt.stderr
new file mode 100644
index 0000000000..452409586d
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearNoExt.stderr
@@ -0,0 +1,3 @@
+
+LinearNoExt.hs:3:12: error:
+    Enable LinearTypes to allow linear functions
diff --git a/testsuite/tests/linear/should_fail/LinearPartialSig.hs b/testsuite/tests/linear/should_fail/LinearPartialSig.hs
new file mode 100644
index 0000000000..01dbeddfba
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPartialSig.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearPartialSig where
+
+-- We should suggest that _ :: Multiplicity
+f :: a # _ -> a
+f x = x
diff --git a/testsuite/tests/linear/should_fail/LinearPartialSig.stderr b/testsuite/tests/linear/should_fail/LinearPartialSig.stderr
new file mode 100644
index 0000000000..4d25260bf2
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPartialSig.stderr
@@ -0,0 +1,7 @@
+
+LinearPartialSig.hs:5:13: error:
+    • Found type wildcard ‘_’
+        standing for ‘'Many :: GHC.Types.Multiplicity’
+      To use the inferred type, enable PartialTypeSignatures
+    • In the type ‘a # _ -> a’
+      In the type signature: f :: a # _ -> a
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.hs b/testsuite/tests/linear/should_fail/LinearPatSyn.hs
new file mode 100644
index 0000000000..3e947dba2e
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module LinearPatSyn where
+
+-- Linearity and pattern synonyms should eventually play well together, but it
+-- seems to require changes to the desugarer. So currently pattern synonyms are
+-- disallowed in linear patterns.
+
+pattern P :: b #-> a #-> (a, b)
+pattern P y x = (x, y)
+
+s :: (a, b) #-> (b, a)
+s (P y x) = (y, x)
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr
new file mode 100644
index 0000000000..f7c3aab406
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr
@@ -0,0 +1,6 @@
+
+LinearPatSyn.hs:14:4: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: P y x
+      In an equation for ‘s’: s (P y x) = (y, x)
diff --git a/testsuite/tests/linear/should_fail/LinearPolyType.hs b/testsuite/tests/linear/should_fail/LinearPolyType.hs
new file mode 100644
index 0000000000..bcf46eed9f
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPolyType.hs
@@ -0,0 +1,16 @@
+-- Source: https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-438125526
+{-# LANGUAGE LinearTypes, GADTs, KindSignatures, DataKinds, TypeFamilies, PolyKinds #-}
+module LinearPolyType where
+
+import GHC.Types
+data SBool :: Bool -> Type where
+  STrue :: SBool True
+  SFalse :: SBool False
+
+type family If b t f where
+  If True t _ = t
+  If False _ f = f
+
+dep :: SBool b -> Int # If b One Many -> Int
+dep STrue x = x
+dep SFalse _ = 0
diff --git a/testsuite/tests/linear/should_fail/LinearPolyType.stderr b/testsuite/tests/linear/should_fail/LinearPolyType.stderr
new file mode 100644
index 0000000000..fab6dfcc9b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearPolyType.stderr
@@ -0,0 +1,3 @@
+
+LinearPolyType.hs:15:1: error:
+    Multiplicity coercions are currently not supported
diff --git a/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs b/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs
new file mode 100644
index 0000000000..e143dbd604
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearRecordUpdate where
+
+data R = R { x :: Int, y :: Bool }
+
+shouldFail :: R #-> R
+shouldFail r = r { y = False }
diff --git a/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr b/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr
new file mode 100644
index 0000000000..aa32a9db68
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr
@@ -0,0 +1,5 @@
+
+LinearRecordUpdate.hs:8:12: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘r’
+    • In an equation for ‘shouldFail’: shouldFail r = r {y = False}
diff --git a/testsuite/tests/linear/should_fail/LinearSeq.hs b/testsuite/tests/linear/should_fail/LinearSeq.hs
new file mode 100644
index 0000000000..0f2ed39c93
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearSeq.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearSeq where
+
+bad :: a #-> ()
+bad x = seq x ()
diff --git a/testsuite/tests/linear/should_fail/LinearSeq.stderr b/testsuite/tests/linear/should_fail/LinearSeq.stderr
new file mode 100644
index 0000000000..f6b22b5999
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearSeq.stderr
@@ -0,0 +1,5 @@
+
+LinearSeq.hs:6:5: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘bad’: bad x = seq x ()
diff --git a/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs b/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs
new file mode 100644
index 0000000000..ff3ac9cedb
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE OverloadedLists #-}
+
+module LinearSequenceExpr where
+
+f :: Char #-> Char #-> [Char]
+f x y = [x .. y]
+-- This ought to fail, because `fromList` in base, is unrestricted
diff --git a/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr b/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr
new file mode 100644
index 0000000000..a3fdb4d7df
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr
@@ -0,0 +1,10 @@
+
+LinearSequenceExpr.hs:7:3: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f’: f x y = [x .. y]
+
+LinearSequenceExpr.hs:7:5: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from multiplicity of ‘y’
+    • In an equation for ‘f’: f x y = [x .. y]
diff --git a/testsuite/tests/linear/should_fail/LinearVar.hs b/testsuite/tests/linear/should_fail/LinearVar.hs
new file mode 100644
index 0000000000..7b4cde3647
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearVar.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearVar where
+
+f :: a # m -> b
+f = undefined :: a -> b
diff --git a/testsuite/tests/linear/should_fail/LinearVar.stderr b/testsuite/tests/linear/should_fail/LinearVar.stderr
new file mode 100644
index 0000000000..04014ce79b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearVar.stderr
@@ -0,0 +1,13 @@
+
+LinearVar.hs:5:5: error:
+    • Couldn't match type ‘m’ with ‘'Many’
+      ‘m’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. a -> b
+        at LinearVar.hs:4:1-16
+      Expected type: a # m -> b
+        Actual type: a -> b
+    • In the expression: undefined :: a -> b
+      In an equation for ‘f’: f = undefined :: a -> b
+    • Relevant bindings include
+        f :: a # m -> b (bound at LinearVar.hs:5:1)
diff --git a/testsuite/tests/linear/should_fail/LinearViewPattern.hs b/testsuite/tests/linear/should_fail/LinearViewPattern.hs
new file mode 100644
index 0000000000..737393911b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearViewPattern.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module LinearViewPattern where
+
+-- This is probably inessential. We are just protecting against potential
+-- incorrect Core being emitted by the desugarer. When we understand linear view
+-- pattern better, we will probably want to remove this test.
+
+f :: Bool #-> Bool
+f (not -> True) = True
diff --git a/testsuite/tests/linear/should_fail/LinearViewPattern.stderr b/testsuite/tests/linear/should_fail/LinearViewPattern.stderr
new file mode 100644
index 0000000000..c0aa969741
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearViewPattern.stderr
@@ -0,0 +1,6 @@
+
+LinearViewPattern.hs:11:4: error:
+    • Couldn't match type ‘'Many’ with ‘'One’
+        arising from a non-linear pattern
+    • In the pattern: not -> True
+      In an equation for ‘f’: f (not -> True) = True
diff --git a/testsuite/tests/linear/should_fail/Makefile b/testsuite/tests/linear/should_fail/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/linear/should_fail/TypeClass.hs b/testsuite/tests/linear/should_fail/TypeClass.hs
new file mode 100644
index 0000000000..9752810dc4
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/TypeClass.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE LinearTypes #-}
+module Foo where
+
+data Either a b = Left a | Right b
+
+either :: (a -> c) -> (b -> c) -> Either a b -> c
+either f g (Left a) = f a
+either f g (Right b) = g b
+
+class Iden p where
+  iden :: p a a
+
+instance Iden (->) where
+  iden x = x
+
+class Cat p where
+  comp :: p b c -> p a b -> p a c
+
+instance Cat (->) where
+  comp f g = \x -> f (g x)
+
+class ArrowChoice a where
+    (+++) :: a b c -> a b' c' -> a (Either b b') (Either c c')
+    (|||) :: a b d -> a c d -> a (Either b c) d
+
+instance ArrowChoice (->) where
+--    This doesn't work as |p| is inferred to be |-o| because of |Left|.
+--    Then GHC complains that |f| is not the same type before it realises
+--    that the overall type must be (->)
+--    f +++ g = (Left `comp` f) ||| (Right `comp` g)
+    f +++ g = (comp @(->) Left f) ||| (comp @(->) Right g)
+    (|||) = either
+
+
+-- This shouldn't work
+foo :: a ⊸ a
+foo = iden
diff --git a/testsuite/tests/linear/should_fail/TypeClass.stderr b/testsuite/tests/linear/should_fail/TypeClass.stderr
new file mode 100644
index 0000000000..97ff625686
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/TypeClass.stderr
@@ -0,0 +1,5 @@
+
+TypeClass.hs:45:7: error:
+    • No instance for (Iden (FUN 'One)) arising from a use of ‘iden’
+    • In the expression: iden
+      In an equation for ‘foo’: foo = iden
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
new file mode 100644
index 0000000000..67906053dc
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/all.T
@@ -0,0 +1,29 @@
+broken_multiplicity_syntax = 94  # https://github.com/tweag/ghc/issues/94
+
+test('TypeClass', normal, compile_fail, [''])
+test('Linear11', normal, compile_fail, [''])
+test('Linear13', normal, compile_fail, [''])
+test('Linear17', normal, compile_fail, [''])
+test('Linear1', normal, compile_fail, [''])
+test('Linear2', normal, compile_fail, [''])
+test('Linear5', normal, compile_fail, [''])
+test('Linear7', normal, compile_fail, [''])
+test('Linear9', normal, compile_fail, [''])
+test('LinearNoExt', normal, compile_fail, [''])
+test('LinearAsPat', normal, compile_fail, [''])
+test('LinearLet', normal, compile_fail, [''])
+test('LinearLazyPat', normal, compile_fail, [''])
+test('LinearRecordUpdate', normal, compile_fail, [''])
+test('LinearSeq', normal, compile_fail, [''])
+test('LinearViewPattern', normal, compile_fail, [''])
+test('LinearConfusedDollar', normal, compile_fail, [''])
+test('LinearPatSyn', normal, compile_fail, [''])
+test('LinearGADTNewtype', normal, compile_fail, [''])
+test('LinearPartialSig', expect_broken(broken_multiplicity_syntax), compile_fail, [''])
+test('LinearKind', normal, compile_fail, [''])
+test('LinearVar', expect_broken(broken_multiplicity_syntax), compile_fail, [''])
+test('LinearErrOrigin', expect_broken(broken_multiplicity_syntax), compile_fail, [''])
+test('LinearPolyType', expect_broken([436, broken_multiplicity_syntax]), compile_fail, [''])  # not supported yet (#354)
+test('LinearBottomMult', normal, compile_fail, [''])
+test('LinearSequenceExpr', normal, compile_fail, [''])
+test('LinearIf', normal, compile_fail, [''])
diff --git a/testsuite/tests/linear/should_run/LinearGhci.script b/testsuite/tests/linear/should_run/LinearGhci.script
new file mode 100644
index 0000000000..78f81ef8d2
--- /dev/null
+++ b/testsuite/tests/linear/should_run/LinearGhci.script
@@ -0,0 +1,11 @@
+data T a = MkT a
+:type +v MkT
+:set -XLinearTypes
+:type +v MkT
+:set -XGADTs
+data T a where MkT :: a #-> a -> T a
+:info T
+data T a b m n r = MkT a b m n r
+:set -fprint-explicit-foralls
+-- check that user variables are not renamed (see dataConMulVars)
+:type +v MkT
diff --git a/testsuite/tests/linear/should_run/LinearGhci.stdout b/testsuite/tests/linear/should_run/LinearGhci.stdout
new file mode 100644
index 0000000000..ed5c9cfe64
--- /dev/null
+++ b/testsuite/tests/linear/should_run/LinearGhci.stdout
@@ -0,0 +1,7 @@
+MkT :: a -> T a
+MkT :: a -> T a
+type T :: * -> *
+data T a where
+  MkT :: a #-> a -> T a
+  	-- Defined at <interactive>:6:1
+MkT :: forall a b m n r. a -> b -> m -> n -> r -> T a b m n r
diff --git a/testsuite/tests/linear/should_run/LinearTypeable.hs b/testsuite/tests/linear/should_run/LinearTypeable.hs
new file mode 100644
index 0000000000..69772f7b33
--- /dev/null
+++ b/testsuite/tests/linear/should_run/LinearTypeable.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE LinearTypes, TypeOperators #-}
+module Main (main) where
+
+import Data.Typeable
+import Data.Maybe
+
+x :: Maybe ((Int -> Int) :~: (Int #-> Int))
+x = eqT
+
+main = print (isJust x)
diff --git a/testsuite/tests/linear/should_run/LinearTypeable.stdout b/testsuite/tests/linear/should_run/LinearTypeable.stdout
new file mode 100644
index 0000000000..bc59c12aa1
--- /dev/null
+++ b/testsuite/tests/linear/should_run/LinearTypeable.stdout
@@ -0,0 +1 @@
+False
diff --git a/testsuite/tests/linear/should_run/Makefile b/testsuite/tests/linear/should_run/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/linear/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/linear/should_run/all.T b/testsuite/tests/linear/should_run/all.T
new file mode 100644
index 0000000000..1fbe20581c
--- /dev/null
+++ b/testsuite/tests/linear/should_run/all.T
@@ -0,0 +1,2 @@
+test('LinearTypeable', normal, compile_and_run, [''])
+test('LinearGhci', normal, ghci_script, ['LinearGhci.script'])
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index 8d597ad371..b14b69dc04 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -63,13 +63,15 @@
           []
           (Nothing)
           (PrefixCon
-           [({ DumpParsedAst.hs:7:26-30 }
-             (HsTyVar
-              (NoExtField)
-              (NotPromoted)
-              ({ DumpParsedAst.hs:7:26-30 }
-               (Unqual
-                {OccName: Peano}))))])
+           [(HsScaled
+             (HsLinearArrow)
+             ({ DumpParsedAst.hs:7:26-30 }
+              (HsTyVar
+               (NoExtField)
+               (NotPromoted)
+               ({ DumpParsedAst.hs:7:26-30 }
+                (Unqual
+                 {OccName: Peano})))))])
           (Nothing)))]
        ({ <no location info> }
         [])))))
@@ -253,26 +255,28 @@
           []
           (Nothing)
           (PrefixCon
-           [({ DumpParsedAst.hs:14:25-29 }
-             (HsParTy
-              (NoExtField)
-              ({ DumpParsedAst.hs:14:26-28 }
-               (HsAppTy
-                (NoExtField)
-                ({ DumpParsedAst.hs:14:26 }
-                 (HsTyVar
-                  (NoExtField)
-                  (NotPromoted)
-                  ({ DumpParsedAst.hs:14:26 }
-                   (Unqual
-                    {OccName: f}))))
-                ({ DumpParsedAst.hs:14:28 }
-                 (HsTyVar
-                  (NoExtField)
-                  (NotPromoted)
-                  ({ DumpParsedAst.hs:14:28 }
-                   (Unqual
-                    {OccName: a}))))))))])
+           [(HsScaled
+             (HsLinearArrow)
+             ({ DumpParsedAst.hs:14:25-29 }
+              (HsParTy
+               (NoExtField)
+               ({ DumpParsedAst.hs:14:26-28 }
+                (HsAppTy
+                 (NoExtField)
+                 ({ DumpParsedAst.hs:14:26 }
+                  (HsTyVar
+                   (NoExtField)
+                   (NotPromoted)
+                   ({ DumpParsedAst.hs:14:26 }
+                    (Unqual
+                     {OccName: f}))))
+                 ({ DumpParsedAst.hs:14:28 }
+                  (HsTyVar
+                   (NoExtField)
+                   (NotPromoted)
+                   ({ DumpParsedAst.hs:14:28 }
+                    (Unqual
+                     {OccName: a})))))))))])
           (Nothing)))]
        ({ <no location info> }
         [])))))
@@ -386,6 +390,7 @@
            ({ DumpParsedAst.hs:16:31-39 }
             (HsFunTy
              (NoExtField)
+             (HsUnrestrictedArrow)
              ({ DumpParsedAst.hs:16:31 }
               (HsTyVar
                (NoExtField)
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index a2e4cd1e9e..220a2ecd0b 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -99,12 +99,14 @@
             []
             (Nothing)
             (PrefixCon
-             [({ DumpRenamedAst.hs:9:26-30 }
-               (HsTyVar
-                (NoExtField)
-                (NotPromoted)
-                ({ DumpRenamedAst.hs:9:26-30 }
-                 {Name: DumpRenamedAst.Peano})))])
+             [(HsScaled
+               (HsLinearArrow)
+               ({ DumpRenamedAst.hs:9:26-30 }
+                (HsTyVar
+                 (NoExtField)
+                 (NotPromoted)
+                 ({ DumpRenamedAst.hs:9:26-30 }
+                  {Name: DumpRenamedAst.Peano}))))])
             (Nothing)))]
          ({ <no location info> }
           []))))]
@@ -252,6 +254,7 @@
            ({ DumpRenamedAst.hs:15:20-33 }
             (HsFunTy
              (NoExtField)
+             (HsUnrestrictedArrow)
              ({ DumpRenamedAst.hs:15:20 }
               (HsTyVar
                (NoExtField)
@@ -261,6 +264,7 @@
              ({ DumpRenamedAst.hs:15:25-33 }
               (HsFunTy
                (NoExtField)
+               (HsUnrestrictedArrow)
                ({ DumpRenamedAst.hs:15:25 }
                 (HsTyVar
                  (NoExtField)
@@ -304,6 +308,7 @@
                  ({ DumpRenamedAst.hs:18:28-36 }
                   (HsFunTy
                    (NoExtField)
+                   (HsUnrestrictedArrow)
                    ({ DumpRenamedAst.hs:18:28 }
                     (HsTyVar
                      (NoExtField)
@@ -327,12 +332,14 @@
              ({ DumpRenamedAst.hs:18:42-60 }
               (HsFunTy
                (NoExtField)
+               (HsUnrestrictedArrow)
                ({ DumpRenamedAst.hs:18:42-52 }
                 (HsParTy
                  (NoExtField)
                  ({ DumpRenamedAst.hs:18:43-51 }
                   (HsFunTy
                    (NoExtField)
+                   (HsUnrestrictedArrow)
                    ({ DumpRenamedAst.hs:18:43 }
                     (HsTyVar
                      (NoExtField)
@@ -362,53 +369,56 @@
                []
                (Nothing)
                (PrefixCon
-                [({ DumpRenamedAst.hs:19:10-34 }
-                  (HsParTy
-                   (NoExtField)
-                   ({ DumpRenamedAst.hs:19:11-33 }
-                    (HsForAllTy
-                     (NoExtField)
-                     (HsForAllInvis
+                [(HsScaled
+                  (HsLinearArrow)
+                  ({ DumpRenamedAst.hs:19:10-34 }
+                   (HsParTy
+                    (NoExtField)
+                    ({ DumpRenamedAst.hs:19:11-33 }
+                     (HsForAllTy
                       (NoExtField)
-                      [({ DumpRenamedAst.hs:19:18-19 }
-                        (UserTyVar
-                         (NoExtField)
-                         (SpecifiedSpec)
-                         ({ DumpRenamedAst.hs:19:18-19 }
-                          {Name: xx})))])
-                     ({ DumpRenamedAst.hs:19:22-33 }
-                      (HsFunTy
+                      (HsForAllInvis
                        (NoExtField)
-                       ({ DumpRenamedAst.hs:19:22-25 }
-                        (HsAppTy
-                         (NoExtField)
-                         ({ DumpRenamedAst.hs:19:22 }
-                          (HsTyVar
-                           (NoExtField)
-                           (NotPromoted)
-                           ({ DumpRenamedAst.hs:19:22 }
-                            {Name: f})))
-                         ({ DumpRenamedAst.hs:19:24-25 }
-                          (HsTyVar
-                           (NoExtField)
-                           (NotPromoted)
-                           ({ DumpRenamedAst.hs:19:24-25 }
-                            {Name: xx})))))
-                       ({ DumpRenamedAst.hs:19:30-33 }
-                        (HsAppTy
-                         (NoExtField)
-                         ({ DumpRenamedAst.hs:19:30 }
-                          (HsTyVar
-                           (NoExtField)
-                           (NotPromoted)
-                           ({ DumpRenamedAst.hs:19:30 }
-                            {Name: g})))
-                         ({ DumpRenamedAst.hs:19:32-33 }
-                          (HsTyVar
-                           (NoExtField)
-                           (NotPromoted)
-                           ({ DumpRenamedAst.hs:19:32-33 }
-                            {Name: xx})))))))))))])
+                       [({ DumpRenamedAst.hs:19:18-19 }
+                         (UserTyVar
+                          (NoExtField)
+                          (SpecifiedSpec)
+                          ({ DumpRenamedAst.hs:19:18-19 }
+                           {Name: xx})))])
+                      ({ DumpRenamedAst.hs:19:22-33 }
+                       (HsFunTy
+                        (NoExtField)
+                        (HsUnrestrictedArrow)
+                        ({ DumpRenamedAst.hs:19:22-25 }
+                         (HsAppTy
+                          (NoExtField)
+                          ({ DumpRenamedAst.hs:19:22 }
+                           (HsTyVar
+                            (NoExtField)
+                            (NotPromoted)
+                            ({ DumpRenamedAst.hs:19:22 }
+                             {Name: f})))
+                          ({ DumpRenamedAst.hs:19:24-25 }
+                           (HsTyVar
+                            (NoExtField)
+                            (NotPromoted)
+                            ({ DumpRenamedAst.hs:19:24-25 }
+                             {Name: xx})))))
+                        ({ DumpRenamedAst.hs:19:30-33 }
+                         (HsAppTy
+                          (NoExtField)
+                          ({ DumpRenamedAst.hs:19:30 }
+                           (HsTyVar
+                            (NoExtField)
+                            (NotPromoted)
+                            ({ DumpRenamedAst.hs:19:30 }
+                             {Name: g})))
+                          ({ DumpRenamedAst.hs:19:32-33 }
+                           (HsTyVar
+                            (NoExtField)
+                            (NotPromoted)
+                            ({ DumpRenamedAst.hs:19:32-33 }
+                             {Name: xx}))))))))))))])
                ({ DumpRenamedAst.hs:19:39-45 }
                 (HsAppTy
                  (NoExtField)
@@ -485,24 +495,26 @@
             []
             (Nothing)
             (PrefixCon
-             [({ DumpRenamedAst.hs:21:25-29 }
-               (HsParTy
-                (NoExtField)
-                ({ DumpRenamedAst.hs:21:26-28 }
-                 (HsAppTy
-                  (NoExtField)
-                  ({ DumpRenamedAst.hs:21:26 }
-                   (HsTyVar
-                    (NoExtField)
-                    (NotPromoted)
-                    ({ DumpRenamedAst.hs:21:26 }
-                     {Name: f})))
-                  ({ DumpRenamedAst.hs:21:28 }
-                   (HsTyVar
-                    (NoExtField)
-                    (NotPromoted)
-                    ({ DumpRenamedAst.hs:21:28 }
-                     {Name: a})))))))])
+             [(HsScaled
+               (HsLinearArrow)
+               ({ DumpRenamedAst.hs:21:25-29 }
+                (HsParTy
+                 (NoExtField)
+                 ({ DumpRenamedAst.hs:21:26-28 }
+                  (HsAppTy
+                   (NoExtField)
+                   ({ DumpRenamedAst.hs:21:26 }
+                    (HsTyVar
+                     (NoExtField)
+                     (NotPromoted)
+                     ({ DumpRenamedAst.hs:21:26 }
+                      {Name: f})))
+                   ({ DumpRenamedAst.hs:21:28 }
+                    (HsTyVar
+                     (NoExtField)
+                     (NotPromoted)
+                     ({ DumpRenamedAst.hs:21:28 }
+                      {Name: a}))))))))])
             (Nothing)))]
          ({ <no location info> }
           []))))]
@@ -608,6 +620,7 @@
              ({ DumpRenamedAst.hs:23:31-39 }
               (HsFunTy
                (NoExtField)
+               (HsUnrestrictedArrow)
                ({ DumpRenamedAst.hs:23:31 }
                 (HsTyVar
                  (NoExtField)
diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr
index a23369a65e..689cc4187f 100644
--- a/testsuite/tests/parser/should_compile/KindSigs.stderr
+++ b/testsuite/tests/parser/should_compile/KindSigs.stderr
@@ -274,6 +274,7 @@
         ({ KindSigs.hs:22:8-44 }
          (HsFunTy
           (NoExtField)
+          (HsUnrestrictedArrow)
           ({ KindSigs.hs:22:8-20 }
            (HsParTy
             (NoExtField)
@@ -297,6 +298,7 @@
           ({ KindSigs.hs:22:25-44 }
            (HsFunTy
             (NoExtField)
+            (HsUnrestrictedArrow)
             ({ KindSigs.hs:22:25-28 }
              (HsTyVar
               (NoExtField)
diff --git a/testsuite/tests/parser/should_compile/T14189.stderr b/testsuite/tests/parser/should_compile/T14189.stderr
index fe4d5d861f..f794049568 100644
--- a/testsuite/tests/parser/should_compile/T14189.stderr
+++ b/testsuite/tests/parser/should_compile/T14189.stderr
@@ -41,12 +41,14 @@
             []
             (Nothing)
             (PrefixCon
-             [({ T14189.hs:6:18-20 }
-               (HsTyVar
-                (NoExtField)
-                (NotPromoted)
-                ({ T14189.hs:6:18-20 }
-                 {Name: GHC.Types.Int})))])
+             [(HsScaled
+               (HsLinearArrow)
+               ({ T14189.hs:6:18-20 }
+                (HsTyVar
+                 (NoExtField)
+                 (NotPromoted)
+                 ({ T14189.hs:6:18-20 }
+                  {Name: GHC.Types.Int}))))])
             (Nothing)))
          ,({ T14189.hs:6:24-25 }
            (ConDeclH98
diff --git a/testsuite/tests/polykinds/T6002.hs b/testsuite/tests/polykinds/T6002.hs
index 5a1b0edd3e..f8bf2219bb 100644
--- a/testsuite/tests/polykinds/T6002.hs
+++ b/testsuite/tests/polykinds/T6002.hs
@@ -6,7 +6,7 @@
  - phantom types (when GHC 7.4 arrives, the user-defined kinds)
  - corresponding singleton types
 
-These are basically the constructs from Omega,
+These are basically the constructs from Many,
 reimplemented in Haskell for our purposes. -}
 
 {-# LANGUAGE GADTs, KindSignatures, StandaloneDeriving,
diff --git a/testsuite/tests/printer/T18052a.stderr b/testsuite/tests/printer/T18052a.stderr
index 99aa8b033f..90eea5bb5a 100644
--- a/testsuite/tests/printer/T18052a.stderr
+++ b/testsuite/tests/printer/T18052a.stderr
@@ -11,12 +11,12 @@ Dependent packages: [base-4.15.0.0, ghc-prim-0.6.1,
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 18, types: 53, coercions: 0, joins: 0/0}
+  = {terms: 24, types: 61, coercions: 0, joins: 0/0}
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 7, types: 8, coercions: 0, joins: 0/0}
 T18052a.$b:||: :: forall {a} {b}. a -> b -> (a, b)
 [GblId, Arity=2, Unf=OtherCon []]
-T18052a.$b:||: = GHC.Tuple.(,)
+T18052a.$b:||: = \ (@a) (@b) (x :: a) (y :: b) -> (x, y)
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
 (+++) :: forall {a}. [a] -> [a] -> [a]
diff --git a/testsuite/tests/roles/should_compile/Roles13.stderr b/testsuite/tests/roles/should_compile/Roles13.stderr
index 5004d1aacc..8b55b600a5 100644
--- a/testsuite/tests/roles/should_compile/Roles13.stderr
+++ b/testsuite/tests/roles/should_compile/Roles13.stderr
@@ -1,19 +1,20 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 98, types: 38, coercions: 5, joins: 0/0}
+  = {terms: 98, types: 38, coercions: 6, joins: 0/0}
 
 -- RHS size: {terms: 2, types: 2, coercions: 0, joins: 0/0}
 convert1 :: Wrap Age -> Wrap Age
 [GblId, Arity=1, Unf=OtherCon []]
 convert1 = \ (ds :: Wrap Age) -> ds
 
--- RHS size: {terms: 1, types: 0, coercions: 5, joins: 0/0}
+-- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
 convert :: Wrap Age -> Int
 [GblId, Arity=1, Unf=OtherCon []]
 convert
   = convert1
-    `cast` (<Wrap Age>_R ->_R Roles13.N:Wrap[0] (Roles13.N:Age[0])
+    `cast` (<Wrap Age>_R
+            # <'Many>_N ->_R Roles13.N:Wrap[0] (Roles13.N:Age[0])
             :: (Wrap Age -> Wrap Age) ~R# (Wrap Age -> Int))
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/simplCore/should_compile/T18013.stderr b/testsuite/tests/simplCore/should_compile/T18013.stderr
index 8d6f2931cd..7b5547efe7 100644
--- a/testsuite/tests/simplCore/should_compile/T18013.stderr
+++ b/testsuite/tests/simplCore/should_compile/T18013.stderr
@@ -129,9 +129,9 @@ Rule fired: Class op fmap (BUILTIN)
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 52, types: 106, coercions: 15, joins: 0/1}
+  = {terms: 52, types: 106, coercions: 17, joins: 0/1}
 
--- RHS size: {terms: 37, types: 87, coercions: 15, joins: 0/1}
+-- RHS size: {terms: 37, types: 87, coercions: 17, joins: 0/1}
 mapMaybeRule
   :: forall a b. Rule IO a b -> Rule IO (Maybe a) (Maybe b)
 [GblId,
@@ -164,7 +164,7 @@ mapMaybeRule
                 }
                 }
             })
-         `cast` <Co:11>)
+         `cast` <Co:13>)
       }
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/simplCore/should_compile/T4201.stdout b/testsuite/tests/simplCore/should_compile/T4201.stdout
index ac8cb0b275..14c7c957de 100644
--- a/testsuite/tests/simplCore/should_compile/T4201.stdout
+++ b/testsuite/tests/simplCore/should_compile/T4201.stdout
@@ -1,4 +1,4 @@
   [HasNoCafRefs, LambdaFormInfo: LFReEntrant 1, Arity: 1,
    Strictness: <S,1*U>,
    Unfolding: InlineRule (0, True, True)
-              bof `cast` (Sym (N:Foo[0]) ->_R <T>_R)]
+              bof `cast` (Sym (N:Foo[0]) # <'Many>_N ->_R <T>_R)]
diff --git a/testsuite/tests/simplCore/should_compile/T7360.stderr b/testsuite/tests/simplCore/should_compile/T7360.stderr
index 9caaa16ff1..67d03b746e 100644
--- a/testsuite/tests/simplCore/should_compile/T7360.stderr
+++ b/testsuite/tests/simplCore/should_compile/T7360.stderr
@@ -4,7 +4,7 @@ Result size of Tidy Core
   = {terms: 106, types: 47, coercions: 0, joins: 0/0}
 
 -- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
-T7360.$WFoo3 [InlPrag=INLINE[final] CONLIKE] :: Int -> Foo
+T7360.$WFoo3 [InlPrag=INLINE[final] CONLIKE] :: Int #-> Foo
 [GblId[DataConWrapper],
  Arity=1,
  Caf=NoCafRefs,
diff --git a/testsuite/tests/stranal/should_compile/T16029.stdout b/testsuite/tests/stranal/should_compile/T16029.stdout
index 100b0791ca..77957255c8 100644
--- a/testsuite/tests/stranal/should_compile/T16029.stdout
+++ b/testsuite/tests/stranal/should_compile/T16029.stdout
@@ -1,4 +1,4 @@
-T16029.$WMkT [InlPrag=INLINE[final] CONLIKE] :: Int -> Int -> T
+T16029.$WMkT [InlPrag=INLINE[final] CONLIKE] :: Int #-> Int #-> T
          Tmpl= \ (dt [Occ=Once!] :: Int) (dt [Occ=Once!] :: Int) ->
   = \ (dt [Occ=Once!] :: Int) (dt [Occ=Once!] :: Int) ->
   :: GHC.Prim.Int# -> GHC.Prim.Int#
diff --git a/testsuite/tests/th/T10019.stdout b/testsuite/tests/th/T10019.stdout
index fb87a9bd9a..6acec6d98f 100644
--- a/testsuite/tests/th/T10019.stdout
+++ b/testsuite/tests/th/T10019.stdout
@@ -1 +1 @@
-"Constructor from Ghci1.Option: Ghci1.Some :: forall (a_0 :: *) .\n                                             a_0 -> Ghci1.Option a_0"
+"Constructor from Ghci1.Option: Ghci1.Some :: forall (a_0 :: *) .\n                                             a_0 #-> Ghci1.Option a_0"
diff --git a/testsuite/tests/th/T11345.stdout b/testsuite/tests/th/T11345.stdout
index 1230c63897..f710d847c8 100644
--- a/testsuite/tests/th/T11345.stdout
+++ b/testsuite/tests/th/T11345.stdout
@@ -3,8 +3,8 @@ data Main.GADT (a_0 :: *) where
                    GHC.Types.Int -> Main.GADT GHC.Types.Int
     (Main.:***:) :: GHC.Types.Int ->
                     GHC.Types.Int -> Main.GADT GHC.Types.Int
-Constructor from Main.GADT: (Main.:***:) :: GHC.Types.Int ->
-                                            GHC.Types.Int -> Main.GADT GHC.Types.Int
+Constructor from Main.GADT: (Main.:***:) :: GHC.Types.Int #->
+                                            GHC.Types.Int #-> Main.GADT GHC.Types.Int
 Nothing
 Just (Fixity 7 InfixR)
 1 :****: 4
diff --git a/testsuite/tests/th/T14888.stderr b/testsuite/tests/th/T14888.stderr
index 4df1e669dc..f58d0c8b45 100644
--- a/testsuite/tests/th/T14888.stderr
+++ b/testsuite/tests/th/T14888.stderr
@@ -7,4 +7,4 @@ T14888.hs:18:22-60: Splicing expression
     "class T14888.Functor' (f_0 :: * -> *)
     where T14888.fmap' :: forall (a_1 :: *) (b_2 :: *) .
                           (a_1 -> b_2) -> f_0 a_1 -> f_0 b_2
-instance T14888.Functor' ((->) r_3 :: * -> *)"
+instance T14888.Functor' ((->) r_3)"
diff --git a/testsuite/tests/th/TH_reifyLinear.hs b/testsuite/tests/th/TH_reifyLinear.hs
new file mode 100644
index 0000000000..c551ad9235
--- /dev/null
+++ b/testsuite/tests/th/TH_reifyLinear.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE LinearTypes #-}
+module TH_reifyLinear where
+
+import Language.Haskell.TH
+import System.IO
+
+type T = Int #-> Int
+
+$(
+    do x <- reify ''T
+       runIO $ hPutStrLn stderr $ pprint x
+       return []
+ )
diff --git a/testsuite/tests/th/TH_reifyLinear.stderr b/testsuite/tests/th/TH_reifyLinear.stderr
new file mode 100644
index 0000000000..ed7866bfa8
--- /dev/null
+++ b/testsuite/tests/th/TH_reifyLinear.stderr
@@ -0,0 +1 @@
+type TH_reifyLinear.T = GHC.Types.Int #-> GHC.Types.Int
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 46fbcf7073..bd279e1128 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -64,6 +64,7 @@ test('TH_spliceD2', [], multimod_compile, ['TH_spliceD2', '-v0'])
 
 test('TH_reifyDecl1', normal, compile, ['-v0'])
 test('TH_reifyDecl2', normal, compile, ['-v0'])
+test('TH_reifyLinear', normal, compile, ['-v0'])
 test('TH_reifyLocalDefs', normal, compile, ['-v0'])
 test('TH_reifyLocalDefs2', normal, compile, ['-v0'])
 
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
index 119c6b91e5..8182d7c992 100644
--- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
@@ -36,10 +36,6 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where const :: forall a b. a -> b -> a
         ($) (_ :: [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: Integer)
-          where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: Integer)
-          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         ($!) (_ :: [Integer] -> Integer)
           where ($!) :: forall a b. (a -> b) -> a -> b
         curry (_ :: (t0, [Integer]) -> Integer) (_ :: t0)
@@ -48,6 +44,10 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
         flip (_ :: [Integer] -> t0 -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
+        return (_ :: Integer)
+          where return :: forall (m :: * -> *) a. Monad m => a -> m a
+        pure (_ :: Integer)
+          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         (>>=) (_ :: [Integer] -> a8) (_ :: a8 -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
                          Monad m =>
@@ -114,14 +114,14 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: [Integer] -> Integer) (_ :: t0)
-          where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: [Integer] -> Integer) (_ :: t0)
-          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         uncurry (_ :: a3 -> b3 -> [Integer] -> Integer) (_ :: (a3, b3))
           where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
         ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
           where ($!) :: forall a b. (a -> b) -> a -> b
+        return (_ :: [Integer] -> Integer) (_ :: t0)
+          where return :: forall (m :: * -> *) a. Monad m => a -> m a
+        pure (_ :: [Integer] -> Integer) (_ :: t0)
+          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 
 abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Integer -> [Integer] -> Integer
@@ -152,10 +152,6 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where const :: forall a b. a -> b -> a
         ($) (_ :: Integer -> [Integer] -> Integer)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: [Integer] -> Integer)
-          where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: [Integer] -> Integer)
-          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         ($!) (_ :: Integer -> [Integer] -> Integer)
           where ($!) :: forall a b. (a -> b) -> a -> b
         curry (_ :: (t0, Integer) -> [Integer] -> Integer) (_ :: t0)
@@ -164,6 +160,10 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
         flip (_ :: Integer -> t0 -> [Integer] -> Integer) (_ :: t0)
           where flip :: forall a b c. (a -> b -> c) -> b -> a -> c
+        return (_ :: [Integer] -> Integer)
+          where return :: forall (m :: * -> *) a. Monad m => a -> m a
+        pure (_ :: [Integer] -> Integer)
+          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         (>>=) (_ :: Integer -> a8)
               (_ :: a8 -> Integer -> [Integer] -> Integer)
           where (>>=) :: forall (m :: * -> *) a b.
@@ -234,12 +234,12 @@ abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           where seq :: forall a b. a -> b -> b
         ($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($) :: forall a b. (a -> b) -> a -> b
-        return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
-          where return :: forall (m :: * -> *) a. Monad m => a -> m a
-        pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
-          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
         uncurry (_ :: a3 -> b3 -> Integer -> [Integer] -> Integer)
                 (_ :: (a3, b3))
           where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
         ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
           where ($!) :: forall a b. (a -> b) -> a -> b
+        return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
+          where return :: forall (m :: * -> *) a. Monad m => a -> m a
+        pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
+          where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b4ac6c9916..8d7c1f573f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -386,7 +386,7 @@ test('holes2', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -
 test('holes3', normalise_version('base'), compile_fail, ['-fno-max-valid-hole-fits -funclutter-valid-hole-fits'])
 test('hole_constraints', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -funclutter-valid-hole-fits'])
 test('hole_constraints_nested', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -funclutter-valid-hole-fits'])
-test('valid_hole_fits', [extra_files(['ValidHoleFits.hs'])],
+test('valid_hole_fits', extra_files(['ValidHoleFits.hs']),
     multimod_compile, ['valid_hole_fits','-fdefer-type-errors -fno-max-valid-hole-fits'])
 test('local_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits'])
 test('subsumption_sort_hole_fits', normal, compile, ['-fdefer-type-errors -fno-max-valid-hole-fits -fsort-by-subsumption-hole-fits'])
diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
index 233f8e23d2..adb507ea92 100644
--- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
@@ -37,12 +37,12 @@ constraint_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           where const :: forall a b. a -> b -> a
         ($) (_ :: [a] -> a)
           where ($) :: forall a b. (a -> b) -> a -> b
+        ($!) (_ :: [a] -> a)
+          where ($!) :: forall a b. (a -> b) -> a -> b
         return (_ :: a)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
         pure (_ :: a)
           where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
-        ($!) (_ :: [a] -> a)
-          where ($!) :: forall a b. (a -> b) -> a -> b
         id (_ :: [a] -> a)
           where id :: forall a. a -> a
         head (_ :: [[a] -> a])
diff --git a/testsuite/tests/typecheck/should_compile/holes.stderr b/testsuite/tests/typecheck/should_compile/holes.stderr
index 9f4422909f..77a6fc9a40 100644
--- a/testsuite/tests/typecheck/should_compile/holes.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes.stderr
@@ -54,6 +54,8 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
         LT :: Ordering
         EQ :: Ordering
         GT :: Ordering
+        One :: GHC.Types.Multiplicity
+        Many :: GHC.Types.Multiplicity
         () :: ()
         lines :: String -> [String]
         unlines :: [String] -> String
diff --git a/testsuite/tests/typecheck/should_compile/holes3.stderr b/testsuite/tests/typecheck/should_compile/holes3.stderr
index fe6aaf391e..874fd4459f 100644
--- a/testsuite/tests/typecheck/should_compile/holes3.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes3.stderr
@@ -57,6 +57,8 @@ holes3.hs:11:15: error:
         LT :: Ordering
         EQ :: Ordering
         GT :: Ordering
+        One :: GHC.Types.Multiplicity
+        Many :: GHC.Types.Multiplicity
         () :: ()
         lines :: String -> [String]
         unlines :: [String] -> String
diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
index 51e29fd3a2..9e97fb51ff 100644
--- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
+++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
@@ -71,6 +71,11 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @'GHC.Types.LiftedRep @[Integer] @Integer
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         return (_ :: Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
           with return @((->) [Integer]) @Integer
@@ -81,11 +86,6 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
           with pure @((->) [Integer]) @Integer
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @'GHC.Types.LiftedRep @[Integer] @Integer
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
         id (_ :: [Integer] -> Integer)
           where id :: forall a. a -> a
           with id @([Integer] -> Integer)
@@ -167,6 +167,11 @@ refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           with ($) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
+        ($!) (_ :: Integer -> [Integer] -> Integer)
+          where ($!) :: forall a b. (a -> b) -> a -> b
+          with ($!) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
+          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
         return (_ :: [Integer] -> Integer)
           where return :: forall (m :: * -> *) a. Monad m => a -> m a
           with return @((->) Integer) @([Integer] -> Integer)
@@ -177,11 +182,6 @@ refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
           with pure @((->) Integer) @([Integer] -> Integer)
           (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
            (and originally defined in ‘GHC.Base’))
-        ($!) (_ :: Integer -> [Integer] -> Integer)
-          where ($!) :: forall a b. (a -> b) -> a -> b
-          with ($!) @'GHC.Types.LiftedRep @Integer @([Integer] -> Integer)
-          (imported from ‘Prelude’ at refinement_hole_fits.hs:1:8-30
-           (and originally defined in ‘GHC.Base’))
         id (_ :: Integer -> [Integer] -> Integer)
           where id :: forall a. a -> a
           with id @(Integer -> [Integer] -> Integer)
diff --git a/testsuite/tests/typecheck/should_fail/T17021.stderr b/testsuite/tests/typecheck/should_fail/T17021.stderr
index 712858b19f..12d6d687d8 100644
--- a/testsuite/tests/typecheck/should_fail/T17021.stderr
+++ b/testsuite/tests/typecheck/should_fail/T17021.stderr
@@ -1,14 +1,6 @@
 
 T17021.hs:18:5: error:
-    Cannot use function with levity-polymorphic arguments:
-      T17021.MkT :: Int -> T
-    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
-    are eta-expanded internally because they must occur fully saturated.
-    Use -fprint-typechecker-elaboration to display the full expression.)
-    Levity-polymorphic arguments: Int :: TYPE (Id 'LiftedRep)
-
-T17021.hs:18:9: error:
     A levity-polymorphic type is not allowed here:
       Type: Int
       Kind: TYPE (Id 'LiftedRep)
-    In the type of expression: 42
+    When trying to create a variable of type: Int
diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
index 70746fd60a..a33a957e9d 100644
--- a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
+++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
@@ -1,8 +1,6 @@
 
 UnliftedNewtypesLevityBinder.hs:16:7: error:
-    Cannot use function with levity-polymorphic arguments:
-      IdentC :: a -> Ident a
-    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
-    are eta-expanded internally because they must occur fully saturated.
-    Use -fprint-typechecker-elaboration to display the full expression.)
-    Levity-polymorphic arguments: a :: TYPE r
+    A levity-polymorphic type is not allowed here:
+      Type: a
+      Kind: TYPE r
+    When trying to create a variable of type: a
diff --git a/testsuite/tests/typecheck/should_run/T14236.stdout b/testsuite/tests/typecheck/should_run/T14236.stdout
index a168ea8d04..ffa0e65dc9 100644
--- a/testsuite/tests/typecheck/should_run/T14236.stdout
+++ b/testsuite/tests/typecheck/should_run/T14236.stdout
@@ -1,3 +1,3 @@
-((->) 'LiftedRep 'LiftedRep Int,Char)
-((->) 'IntRep 'LiftedRep Int#,Char)
+(FUN 'Many 'LiftedRep 'LiftedRep Int,Char)
+(FUN 'Many 'IntRep 'LiftedRep Int#,Char)
 Int# -> [Char]
diff --git a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
index 515738e98e..7769b78eb9 100644
--- a/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
+++ b/testsuite/tests/typecheck/should_run/TestTypeableBinary.stdout
@@ -5,7 +5,7 @@ good: Maybe
 good: TYPE
 good: RuntimeRep
 good: 'IntRep
-good: (->) 'LiftedRep 'LiftedRep
+good: FUN 'Many 'LiftedRep 'LiftedRep
 good: Proxy * Int
 good: Proxy (TYPE 'IntRep) Int#
 good: *