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.

1 files changed, 11 insertions, 11 deletions

diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 7c0eaa7912..2edce28eac 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -620,7 +620,7 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
       where newTyVars = replicateM refLvl $ setLvl <$>
                             (newOpenTypeKind >>= newFlexiTyVar)
             setLvl = flip setMetaTyVarTcLevel hole_lvl
-            wrapWithVars vars = mkVisFunTys (map mkTyVarTy vars) hole_ty
+            wrapWithVars vars = mkVisFunTysMany (map mkTyVarTy vars) hole_ty
 
     sortFits :: SortingAlg    -- How we should sort the hole fits
              -> [HoleFit]     -- The subs to sort
@@ -758,34 +758,34 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
         do { traceTc "lookingUp" $ ppr el
            ; maybeThing <- lookup el
            ; case maybeThing of
-               Just id | not_trivial id ->
-                       do { fits <- fitsHole ty (idType id)
+               Just (id, id_ty) | not_trivial id ->
+                       do { fits <- fitsHole ty id_ty
                           ; case fits of
-                              Just (wrp, matches) -> keep_it id wrp matches
+                              Just (wrp, matches) -> keep_it id id_ty wrp matches
                               _ -> discard_it }
                _ -> discard_it }
         where
           -- We want to filter out undefined and the likes from GHC.Err
           not_trivial id = nameModule_maybe (idName id) /= Just gHC_ERR
 
-          lookup :: HoleFitCandidate -> TcM (Maybe Id)
-          lookup (IdHFCand id) = return (Just id)
+          lookup :: HoleFitCandidate -> TcM (Maybe (Id, Type))
+          lookup (IdHFCand id) = return (Just (id, idType id))
           lookup hfc = do { thing <- tcLookup name
                           ; return $ case thing of
-                                       ATcId {tct_id = id} -> Just id
-                                       AGlobal (AnId id)   -> Just id
+                                       ATcId {tct_id = id} -> Just (id, idType id)
+                                       AGlobal (AnId id)   -> Just (id, idType id)
                                        AGlobal (AConLike (RealDataCon con)) ->
-                                           Just (dataConWrapId con)
+                                           Just (dataConWrapId con, dataConNonlinearType con)
                                        _ -> Nothing }
             where name = case hfc of
                            IdHFCand id -> idName id
                            GreHFCand gre -> gre_name gre
                            NameHFCand name -> name
           discard_it = go subs seen maxleft ty elts
-          keep_it eid wrp ms = go (fit:subs) (extendVarSet seen eid)
+          keep_it eid eid_ty wrp ms = go (fit:subs) (extendVarSet seen eid)
                                  ((\n -> n - 1) <$> maxleft) ty elts
             where
-              fit = HoleFit { hfId = eid, hfCand = el, hfType = (idType eid)
+              fit = HoleFit { hfId = eid, hfCand = el, hfType = eid_ty
                             , hfRefLvl = length (snd ty)
                             , hfWrap = wrp, hfMatches = ms
                             , hfDoc = Nothing }