Make the design of defaulting explicit
GHC does some "defaulting" on kind and runtimerep variables, but the design has never really been described. Yet in !6851 (closed), !6866 (merged) it became clear that we didn't really know what we were doing. This ticket sets out a design, and articulates a choice.
See "The Choice" below.
Definitions

The kind components of a type ty are those kinds ki where
 ki is the kind of a unification variable free in ty. (A skolem is certain to be global.)
 ki is the kind of a localforall’d binder in ty. e.g.
(forall (a::ki). blah) > Int
 ki is the kind of a coercion in ty. e.g.
ty > (co :: ki)

The “dependent type variables of a type” ty are those that appear free ty’s kind components. That’s what
Note [Dependent type variables]
says. 
The “runtimereps components of a type” ty is a set of types (all of kind
RuntimeRep
) that are The argument of
TYPE
, which is itself in the kind component of ty  The
RuntimeRep
arguments of(>)
in ty.
 The argument of

The “multiplicitity components of a type” ty is a set of types (all of kind
Multiplicity
) that appear as the multiplicity argument of(>)
in ty.
Common ground, especially for inferring the type of a letbound definition without a type signature

There are three places that defaulting can take place
 LocalDefaulting, when kindchecking a type signature, or when inferring the type of a letbinding. Mainly done in
quantifyTyVars
today. This defaulting happens before any quantification takes place; it can thus affect which variables end up quantified in a variable's type.  TypeClassDefaulting. Done at toplevel only (
simplifyTop
), used to default e.g.Num a
by fixinga := Integer
. Driven by ‘default’ declarations.  FinalZonkDefaulting. Done by the final zonk. This is a catchall defaulting step, looking for any variable not yet filled in. Today, it works by:
 Default
(alpha :: RuntimeRep) := LiftedRep
 Default
(alpha :: Levity) := Lifted
 Default
(alpha :: k) := Any @k
 Default
 LocalDefaulting, when kindchecking a type signature, or when inferring the type of a letbinding. Mainly done in

Local and global type variables.

A local type variable has a level number equal to the ambient level of the binding; equivalently, these are the the variables that do not appear in the environment.

A global type variable has a level number strictly less than the ambient level of the binding; equivalently, these are free in the environment.

Only local variables are affected by our treatment here. Global variables are entirely unaffected.


When quantifying a type, every local type variable must be:
 (P) Promoted to the outer level (thereby becoming global), or
 (D) Defaulted to a closed type (LocalDefaulting), or
 (Q) Quantified

Monomorphism restriction. If the monomorphism restriction applies due to the syntax of a letbinding, promote all local variables free in any constraint. These promoted variables are now considered global.

Determined type variables. A type variable tv is determined iff fixing global type variables would uniquely determine tv. This happens via fundeps: with
C a b  a > b
, and constraintC t1 t2
, where tyvars(t1) are all global, then injectivetyvars(t2) are determined. Notes: Equality constraints
~
have a bidirectional fundep, as if we hadclass a ~ b  a > b, b > a
.  The injectivetyvars computation is not yet implemented. #20668 tracks this flaw.
 HEAD (pre !5899) looks only at equality constraints for the "determined" calculation. !5899 broadens to look at all classes with fundeps.
If tv is determined by global tyvars, promote tv (so that it too becomes global). We promote these determined variables to avoid Henry Ford polymorphism ("any type
a
as long as it'sInt
"), but quantifying them is not unsound.Because promotion adds new global variables, the set of determined variables may increase; so we need to repeat the step of deciding determined variables until a fixpoint is reached.
 Equality constraints

Concrete#
constraints. We never quantify over a variable mentioned in aConcrete#
constraint, because the whole point ofConcrete#
is to prevent such quantification. Instead we must either default or promote it (see below). 
Flag control
 NoPolyKinds => do not quantify over variables free in kind component
 NoPolyRepresentations => do not quantify over variables free in runtimerep components
 NoPolyMultiplicities => do not quantify over variables free in multiplicity components.
For all of these variables, if we do not quantify over them, we must either default or promote them. See below for this choice.

We always default multiplicity variables (with NoPolyMultiplicities); we never promote them. Why? It is very hard to learn more about a multiplicity from usage sites.
How to default
We have a free choice about whether to Default (D) or Promote (P) the free local unification variables of:
 kind components (with NoPolyKinds)
 runtimerep components (with NoPolyRepresentations)
 multiplicity components (with NoPolyMultiplicities)
 the argument of a
Concrete#
constraint
To promote (P) is easy: just promote each of the variables.
To default (D) we take two steps: For each kind component ki
 Promote its free variables, just as in (P)
 Add a new wanted constraint e.g.
rr ~ LiftedRep
Notes
 If
rr
is a local unification variable, a very common case, we can just unify itki := LiftedRep
. This is just an efficiency shortcut. But if we can't unify it we still emit the equality constraint, which ensures that even if ki isF blah
, which doesn’t yet reduce, we’ll check that it eventually reduces toLiftedRep
, the default.  Note carefully that we do not default all type variables of kind
RuntimeRep
, nor do we restrict quantification over them. Rather, we promote and default the runtimerep components as defined above. This makes #17201 work as expected. E.g.
When inferringf1 :: forall (p :: RuntimeRep > Type) (r :: RuntimeRep). p r > p r f1 x = x  Inferred type g1 :: forall (p :: RuntimeRep > Type) (r :: RuntimeRep). p r > p r g1 = f1
g1
's type we will quantify overr :: RuntimeRep
; in this example there are noRuntimeRep
components.
Similarly for
 each runtimerep component rr (constraint is
rr ~ LiftedRep
);  each multiplicity component m (constraint:
m ~ Many
);  each kind component (with NoPolyKinds) (constraint
Concrete# ki
);
We do not do this for Concrete#
constraints, which can be controlled by the classbased default
mechanism.
Alternative, less preferred defaulting strategy
An alternative approach to defaulting is to use kinddirected defaulting during quantification. This is what is done today, where quantifyTyVars
takes variables it cannot quantify and tries to default them:

(alpha :: Type) := Type
(with NoPolyKinds) (alpha :: RuntimeRep) := LiftedRep
(alpha :: Levity) := Lifted
(alpha :: Multiplicity) := Many
The problem with this approach is that it requires looking at the kind during quantification. If that kind is F beta
, where beta
will be learned later, we might miss an opportunity to default, because we learn only later that, say, F beta
really is Multiplicity
. This alternative seems bound to be fragile (this can be observed in GHC today). Example:
{# LANGUAGE RankNTypes, StandaloneKindSignatures #}
{# LANGUAGE DataKinds, LinearTypes, TypeFamilies, PartialTypeSignatures #}
module Bug where
import Data.Kind
import GHC.Exts
import GHC.Types
import Data.Proxy
type Multy :: () > Type
type family Multy a where
Multy '() = Multiplicity
type Fun :: forall (a :: ()) > Multy a > Type > Type > Type
type family Fun a m where
Fun '() m = FUN m
myId1 :: Proxy _u > Fun _u _ a a
myId1 (Proxy :: Proxy '()) x = x
myId2 :: Proxy '() > Fun '() _ a a
myId2 (Proxy :: Proxy '()) x = x
GHC infers myId1
to be multiplicity polymorphic, because it doesn't learn that _u := '()
until after kindgeneralizing the type. On the other hand myId2
is multiplicitymonomorphic.
The Choice: promoting vs defaulting
Finally we have a free design choice: should we promote, or default? That is, do we add the extra constraints used for defaulting? (That is, we always promote. The only question is about those extra constraints.)
Simon prefers (D) Default. Reasons

It makes reasoning more local. You can figure out what a type signature means without looking to see how it is used.

It eliminates the nasty possibility of an inferred type like
f :: forall a. Foo LiftedRep a => blah
, where we have aninstance Foo LiftedRep t
. This can happen if we inferf :: forall a. Foo rr a => blah
, whererr
is still a unification variable, ultimately set toLiftedRep
On point (2) note that we have this possibility today:
class C a b where
meth :: a > b > ()
instance C a Integer where
meth _ _ = ()
x = 5  MR
f z y = (meth z y, x + y)
GHC infers f :: C a Integer => a > Integer > ((), Integer)
, exactly this point is worried about.
Richard prefers (P) Promote. Reasons:
 It allows GHC to accept more programs. Example:
f x = x
g () = f 3#
We see from the usage site that f
should have type forall (a :: TYPE IntRep). a > a
. Another, more elaborate example is below. Note that the representationpolymorphic Num
is a fine idea. See proposal at https://github.com/ghcproposals/ghcproposals/pull/30 and ticket #12708.
class Num (a :: TYPE rep) where ...  methods as today
someFun :: Int# > ...
someFun z = ... let frob x y = x + (y * 2) in frob 3 4 + z ...
We need to know that frob
should work over unboxed numbers, but this knowledge comes only from usage sites.

(P) is more in keeping with the original spirit of Haskell. The monomorphism restriction (MR) imposes a "do not quantify" dictum like e.g. NoPolyRepresentations would. It currently uses strategy (P). But we could imagine (we are not doing this. thought experiment only!) changing the MR to use (D) instead. Then,
x = 5
would always beInteger
: this is more local and simpler. But it would be a real pain to users, and not just around legacy code.I (Richard) want a future where more people use unlifted and unboxed types. (Unlifted especially.) If we promote rather than default, it will be easier to write functions over unlifted and unboxed types.
Other points
When kindgeneralising an explicit userwritten type signature: If we promote (P) we could allow
f :: forall a. a > a
f @(a :: UnliftedType) x = x
where the usesite in f
’s defn fixes the monomorphic (promoted) representation variable in f
’s type sig.
Or we could default more aggressively to make the “complete” type signature more complete.
Implementation
Turning to implementation, here is a plan for GHC.Tc.Solver.decideQuantification

Identify all defaultable "components", namely
 (a) kind components (with NoPolyKinds)
 (b) runtimerep components (with NoPolyRepresentations)
 (c) multiplicity components (with NoPolyMultiplicities)
 (d) the argument of a Concrete# constraint
 (e) constraints that fall under the Monomorphism Restriction, e.g. Num a

Promotion and defaulting. For each such component,
 Promote all its free variables and
 If we are doing defaulting (D), then for (ac), emit an constraint, thus
 (a) Emit
Concrete# ki
for a kind componentki
; this ensures thatki
will eventually be concrete.  (b) Emit
rr ~ LiftedRep
for a runtimerep componentrr
.  (c) Emit
mu ~ Many
for a multiplicity componentmu
 (a) Emit
Question: what do we do with the evidence for these equalities? Simply discard it: the equalities are not required in order to ensure the program is welltyped, according to our basic typing rules. (Here, "basic" means our typing rules without the notquitecompositional levity/representation monomorphism restrictions.) So there's no place we will need the evidence. The equality is there only to force defaulting.
Note: we say "emit a constraint" but we really mean "take a short cut if possible, and emit a constraint if not". Example: rather than emit
rr ~ LiftedRep
dounifyDerived rr LiftedRep
. That will try to unifyrr
(which can be an arbitrary type, remember) withLiftedRep
. This will often succeed, but perhaps not always; e.g. mayberr
isF alpha
andalpha
gets unified later; in this latter (rare) case we do emit a constraint.Note: we need a shortcut for emitting a
Concrete#
constraint. For this short cut it might be helpful to default before promoting, because for local unification varaibles we know that no other constraints will affect them, whereas for global ones we might learn more. Also, if shortcut unification with LiftedRep succeeds, there was no point in promoting (efficiency).Note: we need no special handling of variables of type/kind
RuntimeRep
. Instead, we now treat runtimerep components specially, not variables. 
If we emitted any constraints, simplify the constraints again, in the hope of unlocking further simplification.
Question: when wanteds can simplify wanteds, maybe that means we won't get to (Eq a, Ord a) and can get rid of
mkMinimalBySCs
? 
Find and promote any tyvars that are functionally dependent (via a constraint) on a promoted (global, nonlocal) type variable. This step follows (1) because (1) promotes some variables, which might transitively make others determined.

Find which type variables to quantify: all local (nonpromoted) tyvars free in tautvs, or transitively connected to those by any constraint. (See current
decideQuantifiedTyVars
.) The "transitively dependent" bit is so that we quantify overb
inC a b => a > a
, but not overa
inC a => b > b
. 
Find which constraints to quantify: the ones that mentions any quantified tyvar. Simple.
We should remove all the defaulting from quantifyTyVars
, and use a simplified version of (15) for the other calls to quantifyTyVars
.