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
mniip (f7c8176a) at 17 Jun 08:10
Add a fprintaxiomincomps option (#15546)
... and 506 more commits
This part is unclear: 2257a86d
There used to be a call to tidyVarBndrs
that produced some kind of env that was used to tidy other things (?) and now it's gone. Having no idea what the process did, I worry whether this will have an effect on the incompatible branch computation, since different branches could have different tyvars or something like that.
I've been unable to find any comprehensive documentation on what tidying is/how tidying works, so I'm unable to thoroughly verify whether the changes have been ported correctly. On the other hand I'm not really changing the process by which a branch is tidied, so if it was correct before then it probably also is after...
This is from https://phabricator.haskell.org/D5097, rebased against the current HEAD.