So I've had this idea.
We have an inference rule that turns a single type family equation axiom into a coercion. And then when we reduce a recursive type family, we chain a ton of these together with a transitivity inference rule.
What if instead we had a single inference rule for a coercion that is automatically but deterministically produced from a collection of type family equations. So that e.g. a repetitive unfolding of a recursive type family would be represented with a single coercion (it would still take a linear amount of time to lint, but if we're not linting we get a performance win).
For example, we could introduce:
CbnCo
:: Type  ^ LHS
> [CoAxiom Branched]  ^ List of used axioms
> Int  ^ How many reduction steps we've taken (n)
> Type  ^ RHS
> Coercion
with the semantics that if we applied the callbyneed evaluation strategy to LHS for exactly n steps, then we would arrive at RHS, and we would use exactly the listed axioms.
This is backwards compatible because we can turn an AxiomInstCo
into a CbnCo
with a single axiom and n=1
.
The exact evaluation strategy doesn't matter, as long as it's deterministic in context of a list of available axioms (with the caveat that the typechecker itself will have a larger set of axioms available when producing this elaboration, and having had a smaller axiom set might've led it to produce a different elaboration); and as long as common patterns of using recursive type families actually fold into a relatively small number of CbnCo
's (instead of 1 CbnCo
per TF reduction).
@rae what do you think?
Good observations. Here's an idea for a way forward: it's rare, in practice to need both types in a coercion. We absolutely need to be able to take the type of any term. But if we have a term
e > co
, we can know its type even if we only know the righthand type ofco
. In coercion arguments to functions (an expressionApp xyz (Coercion co)
), we don't need either type: the types of the coercion are fully known by the type ofxyz
. So perhaps we can have different varietals of zapped coercion: a normal coercion (really, it should be called a bicoercion, because it can coerce both ways), a unicoercion which stores only one type (these might need lunicoercion and runicoercion subvarietals, but I would guess that lunicoercions are loony and never needed in practice), and nullicoercions (citation) which store neither type. Note that the possibility of unicoercions and nullicoercions exist for coercions in types exactly the same way that they work in terms.
I've arrived at a similar idea and from a cursory look it seemed like we only need "runicoercions" and "nullicoercions". So I started a prototype implementation. So far it looks like a lot of places depend on being able to randomly look at coercions' end types, and rewriting everything with maybes greatly increases complexity, especially in the linter. Now the original plan was to zap coercions when linter is off, but I feel like that's a terrible idea if there's a lot of difference between behavior in zapping and nonzapping behavior (and there's a lot of difference), so we should be able to lint, at least rudimentarily, core with zapped coercions. And in particular, since coercions can end up in iface files, and different modules could be compiled with different flags, we could end up with coercions that are a mix of zapped and nonzapped ones, and something has to be done about that.
Allow names from GHC.Prim
to be used with GHCi's :doc
by augmenting the wiredin ModIFace with the documentation generated from primops.txt
.
My use case is abusing quasiquotation as a syntactic sugar for [(Name, Maybe Exp)]
, where the names are field names of a record. I need to take apart the RecConE
so that I can act upon the missing fields (If I left them as is GHC would, following the standard, supply the missing fields with bottoms).
For an even more concrete use case see http://hackage.haskell.org/package/partialrecords0.2.2.1/docs/DataPartialTH.html#v:mkFromPartial and the current workaround: http://hackage.haskell.org/package/partialrecords0.2.2.1/docs/src/Data.Partial.TH.html#parseDefs (c.f. fixEq :: (Name, Exp) > Q (Name, Exp)
doing a reify to find the field Name
corresponding to the selector Name
)
GHC seems to parse record constructions/updates differently when DuplicateRecordFields
is in effect, and that seems to reflect in the data returned from expression quasiquotes:
data D = D { fld :: () }
[D { fld = () }]
 without DuplicateRecordFields:
 RecConE Main.D [(Main.fld, ConE GHC.Tuple.())]
 with DuplicateRecordFields:
 RecConE Main.D [(Main.$sel:fld:D, ConE GHC.Tuple.())]
[d { fld = () }]
 without DuplicateRecordFields:
 RecUpdE (UnboundVarE d) [(Main.fld, ConE GHC.Tuple.())]
 with DuplicateRecordFields:
 RecUpdE (UnboundVarE d) [(Main.$sel:fld:D, ConE GHC.Tuple.())]
Of interest is the selector Main.$sel:fld:D
. It has a name characteristic of GHC Core internal names. The quirkiness manifests in that we cannot lookupValueName "$sel:fld:D"
, and the renamer won't in general pick it up if we use Name (mkOccName "$sel:fld:D") NameS
or even Name (mkOccName "$sel:fld:D") $ NameQ $ mkModName "Main"
. Only Name (mkOccName "$sel:fld:D") $ NameG VarName (mkPkgName "main") (mkModName "Main")
will suffice (and that is the thing we receive from the expression quasiquoters above.
Another quirk is that when we try to reify that name we get back a declaration for a different identifier:
reify $ Name (mkOccName "$sel:fld:D") $ NameG VarName (mkPkgName "main") (mkModName "Main")
 VarI Main.fld (AppT (AppT ArrowT (ConT Main.D)) (TupleT 0)) Nothing
Worth noting that if we do try to quasiquote an ambiguous update, we get a descriptive error message:
data D1 = D1 { fld :: () }
data D2 = D2 { fld :: () }
[d { fld = () }]
 Ambiguous record updates not (yet) handled by Template Haskell
 fld = ()
Question is, should TH know about such internal Core names at all and if so how should TH users tackle them.
> :set XTemplateHaskell XGADTs
> $(pure [Language.Haskell.TH.DataD [] (Language.Haskell.TH.mkName "D") [] Nothing [Language.Haskell.TH.GadtC [] [] (Language.Haskell.TH.ConT (Language.Haskell.TH.mkName "D"))] []]);
*** Exception: compiler/typecheck/TcTyClsDecls.hs:2763:1441: Nonexhaustive patterns in (dL > L _ name) : _
Probably a more welcoming error message.
{# LANGUAGE UnliftedNewtypes #}
{# LANGUAGE ExplicitForAll #}
{# LANGUAGE PolyKinds #}
import GHC.Exts
newtype Id (a :: TYPE r) = Id a
foo :: forall r (a :: TYPE r). Id a > Id a
foo x = x
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20191008:
isUnliftedType
Id a_a1g7 :: TYPE r_a1g6
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2229:10 in ghc:Type
A levitypolymorphic type is not allowed here:
Type: Id a
Kind: TYPE r
In the type of binder ‘x’
The issue seems to be specific to binders of types that are unlifted newtypes.
GHC HEAD
Cc @rae
A potential issue is that such a declaration would warrant a dependent axiom:
axiom D:R:FlD :: forall k l (x :: k) (c :: k ~ l). F l (D k x) ~ (x > c)
We might however try and apply something HindleyMilnerish to simplify it to the currently emitted (for the other instance):
axiom D:R:FkD :: forall k (x :: k). F k (D k x) = x
But I am not sure if this would suffice to later use this axiom, or let alone if all possible elaborations the type(kind) checker could make on (x :: k) ~ (y :: l)
could even be simplified out this way.
When kind checking associated type declarations in an instance
declaration, the instance context seems to be ignored.
Minimal complete example:
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeApplications #}
class C (k :: *) (a :: *) where
type F k a :: k
data D k (x :: k)
instance C k (D k x) where
type F k (D k x) = x  good
instance (k ~ l) => C l (D k x) where
type F l (D k x) = x  bad
{
b.hs:11:22: error:
• Expected kind ‘l’, but ‘x’ has kind ‘k’
• In the type ‘x’
In the type instance declaration for ‘F’
In the instance declaration for ‘C l (D k x)’

11  type F l (D k x) = x  bad
 ^
}
The second instance should kindcheck (it has better instance resolution properties than the first which is why we want it).
Tested on GHC 8.6.5 and GHC HEAD
mniip (f5d5f281) at 28 Jun 10:52
Fix documentation
mniip (e86adc57) at 28 Jun 10:50
Explicitly number equations when printing axiom incompatibilities
On a second though an even better idea would be:
type family (==) (a :: k) (b :: k) :: Bool
where
{ #0 } (==) (f a) (g b) = (f == g) && (a == b)
{ #1 } (==) a a = 'True
 incompatible with: #0
How about:
type family (==) (a :: k) (b :: k) :: Bool
where
(==) (f a) (g b) = (f == g) && (a == b)  #0
(==) a a = 'True  #1
 incompatible indices: #0
Well it isn't specifically an error message, this is additional information hidden behind a flag...
The user guide documentation mentions:
The comment after each equation refers to the indices (0indexed) of preceding equations it is incompatible with.
We have a list of equations so it's pretty natural to talk about indices, and, in haskell at least, indices start from 0.
Done @bgamari
mniip (5bc19cbe) at 17 Jun 12:59
Fix test