Implement the Unlifted Newtypes proposal
Needs ReviewPublic

Authored by andrewthad on Jun 3 2018, 8:01 AM.

Details

Summary

This is proposal 13 on the ghc-proposals repo and is fully described there.

Test Plan

Use the unit tests that are provided in this patch

Diff Detail

There are a very large number of changes, so older changes are hidden. Show Older Changes

No worries! Since I plan on using this feature, I'd like for it to be correct 😄. Thanks for all the feedback.

compiler/deSugar/Desugar.hs
543 ↗(On Diff #19262)

Thanks for pointing this out. That makes a lot of sense that there's a place to do this. I'll wait for further action on this until a decision on the coerce#/coerce issue is made.

550 ↗(On Diff #19262)

The reason I had in mind was the one David listed. I don't think the one Richard gave is accurate. I believe that GHC handles map coerce# fine. I had not considered that a type variable could be marked as Inferred. Indeed, I didn't even realize this was possible. Marking a type argument as Inferred seems a little magic. Can an ordinary user write a function with an Inferred type argument? How do I know from looking at haddocks whether or not an argument is eligible for visible type application? What other functions is this done for? I'm going to research this a little more since I just learned about it. I'm not terribly partial to either solution, so whoever's domain this falls under, I'm happy to let them make the decision.

libraries/ghc-prim/GHC/Types.hs
285

I had forgotten that it was possible to write things like the Coercion Foo Maybe that David suggests. I'm going to change this back, but would it be preferable to do:

class Coercible a b

or

class Coercible (a :: k) (b :: k)

I think the second one is actually more accurate since the first one is equivalent to

class Coercible (a :: k) (b :: j)

Which doesn't match the wired-in type.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
2

There aren't any lifted types involved. I'm not sure where this error message comes from. What I would expect is that the type-checker would unify the kind of Foo, which is (TYPE a0), with the kind of (# Int#, Foo #), which is TYPE (TupleRep '[IntRep, a0]), in an attempt to solve for a0`. Then we would get:

a0 ~ '[IntRep, a0]

Which should lead to a "Cannot create infinite type" error. But this doesn't actually end up happening. I wonder if the Foo inside the data constructor is assigned kind TYPE LiftedRep. That may explain it. I'll investigate this further.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
3

Should I just replace the word "primitive" with something else? Maybe "function"?

testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilySigRun.hs
1 ↗(On Diff #19262)

This differs from UnliftedNewtypesDependentFamilyRun only in its use of a kind signature. I originally separated these out because it made tracing the typechecker easier, but I'll combine these two for clarity.

andrewthad added inline comments.Fri, Jan 4, 9:16 AM
libraries/ghc-prim/GHC/Types.hs
285

I think we both responded to Simon's comment at the same time. I'll plan on just reverting this change unless someone feels strongly about doing class Coercible (a :: k) (b :: k) instead.

goldfire added inline comments.Fri, Jan 4, 9:21 AM
libraries/ghc-prim/GHC/Types.hs
285

Actually, I think putting the kind variables in explicitly is an improvement. Good idea.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr
3

That's good by me. Thanks.

dfeuer added inline comments.Fri, Jan 4, 10:49 AM
libraries/ghc-prim/GHC/Types.hs
285

Are those kind variables visible? Honestly, I think we should bite the bullet and only let variables be visible if they're explicitly quantified by forall......

why is the generalized version of the operation named coerce# instead of eg the coerceLevPoly? Do we want to make this operation only available when magicHash syntax is allowed? AFAIK, the levity polymorphic coerce should always be type safe to use ... so unlike a lot of memory read/write stuff that can doo out of bound reads etc, I dont think it should be magic hashed unless we want to discourage userland uses thereof (which would be fine for me either way).

I kinda view # suffixed names in haskell/ghc land as providing a 3 foot tall fence around things that you maybe dont wanna work with unless you know you need to.

Sorry to add to your pile of TODOs, but I just noticed that this patch actually fixes a Trac ticket that's not listed in the Diff description: Trac #15883. Specifically, this test case:

{-# Language RankNTypes     #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds      #-}

import GHC.Exts

newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)

That currently panics on GHC HEAD, but with this patch, it just produces an error message:

$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )

Bug.hs:7:50: error:
    • Expected a type, but ‘a’ has kind ‘TYPE rep’
    • In the type ‘(forall (a :: TYPE rep). a)’
      In the definition of data constructor ‘MkFoo’
      In the newtype declaration for ‘Foo’
  |
7 | newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
  |                                                  ^

Even better, if you enable UnliftedNewtypes, then it compiles!

andrewthad updated this revision to Diff 19264.Sat, Jan 5, 1:15 PM
  • several documentation-related fixes, additional tests, remove MagicHash extension from modules that do not need it
andrewthad marked 7 inline comments as done.Sat, Jan 5, 1:47 PM

I've added some more tests and made some very minor improvements to docs. Currently failing test are:

should_compile/UnliftedNewtypesUnassociatedFamily.run  UnliftedNewtypesUnassociatedFamily [exit code non-0] (normal)
should_fail/T14048c.run                                T14048c [exit code 0] (normal)
should_fail/T14605.run                                 T14605 [stderr mismatch] (normal)

The first two I'll able to figure out. The third one, I'm not sure what's going on.

Responding to @carter: I find the name coerce# appropriate. The hash suffix is used for all sorts of safe things that work on unlifted types (word2Int#,+#,etc.), and coerce# is no different that these. If you have an unlifted value in scope, you will very likely have MagicHash enabled anyway since writing its type anywhere will likely require MagicHash.

compiler/deSugar/Desugar.hs
550 ↗(On Diff #19262)

After looking into this more, I'm not sold on marking the argument as Inferred. This would be inconsistent with the way that inferred variables are used everywhere else in GHC. There is no way for a user to write a function where a type variable shows up in the type signature but isn't available to VTA. Even the magical $ doesn't do this. That is, GHC rejects ($) @(Int -> Bool) @Int because it wants that RuntimeRep argument.

compiler/typecheck/TcInstDcls.hs
692

You're right that I should some checks here. I've gone ahead and added a test UnliftedNewtypesFamilyKindFail2. Surprisingly, it actually passes already, although we get a doubled error message. Hopefully, that will go away once I make the fix here.

809–810

I'd like to add the example you gave as a test to the test suite to help guide me in fixing this. What is the definition of KindOf that you're using?

compiler/typecheck/TcTyClsDecls.hs
1637

I've added UnliftedNewtypesFamilyKindFail1 to confirm that this fails. Surprisingly, it passes already, but I'll make sure to do the appropriate checks here anyway.

libraries/ghc-prim/GHC/Types.hs
285

I've changed this to class Coercible (a :: k) (b :: k). Let me know if I should go back to class Coercible a b.

testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
23

I've added UnliftedNewtypesUnassociatedFamily and UnliftedNewtypesOverlap to test this. Sadly, the former currently fails. I'm looking into it.

goldfire added inline comments.Sat, Jan 5, 2:44 PM
compiler/deSugar/Desugar.hs
550 ↗(On Diff #19262)

What you say is true today, but it won't be tomorrow. See this accepted proposal. So a library-writer can choose which variables have what level of specificity.

In the case of coerce, I think this choice is justified based on backward-compatibility concerns.

compiler/typecheck/TcInstDcls.hs
692

Where is the check done that already snags this? Maybe we don't need a check here. (And maybe we don't even need it for non-unlifted-newtypes.)

809–810

Sorry:

type KindOf (a :: k) = k
compiler/typecheck/TcTyClsDecls.hs
1637

No -- don't just add checks because I suggested so. Why does is pass already? Is there another place where a check is performed? Without understanding that better, we'll get redundant checks.

libraries/ghc-prim/GHC/Types.hs
285

Looks good to me. Thanks.

andrewthad updated this revision to Diff 19265.Mon, Jan 7, 9:37 AM
  • add UnliftedNewtypesUnifySig test
  • use fresh metavar in tcDataFamHeader
  • add back more kind checks when UnliftedNewtypes in enabled
  • feed more result kinds into kcConDecl
andrewthad marked 12 inline comments as done.Mon, Jan 7, 10:10 AM

I've made several changes involving feeding in result kinds to kcConDecl and adding kind checks back to newtypes when UnliftedNewtypes is enabled. However, UnliftedNewtypesUnifySig is still failing.

compiler/deSugar/Desugar.hs
550 ↗(On Diff #19262)

Ah, I was not aware of that proposal. With that in mind, I'm fine with just having coerce. Its type signature, using to the nomenclature in the Explicit Specificity proposal, would be:

coerce :: forall {r :: RuntimeRep} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b

And once the Explicit Specificity proposal was implemented, users could actually see this type signature in at ghci and in the haddocks. I'm fine with this approach.

compiler/typecheck/TcInstDcls.hs
692

I'm not sure where the other check is, but although it rejects Nat, it accepts Constraint. This was making T14048c fail (well, I had also inadvertently changed tcIsLiftedTypeKind to isLiftedTypeKind). So, this check is necessary for unlifted newtypes as well. I've improved it to do the right thing and require that the kind is of the form TYPE r, for some r.

851

That was the solution I overlooked when I wrote this. Inventing a fresh metavar is a much more elegant than than what I had done. It also prevents a later step from basically unifying res_kind with itself.

compiler/typecheck/TcTyClsDecls.hs
1637

You were correct that it would mess up something. We need to reject

data family D (a :: Type) :: Constraint

in the presence of UnliftedNewtypes. I've changed the code appropriately and add a test UnliftedNewtypesConstraintFamily to confirm that this is now rejected. (tangentially related, is tcIsRuntimeTypeKind a good name for the helper function I've added?) I still don't know why the example using Nat that you gave was rejected, but my hunch is that somewhere else, kindRep_maybe gets called, which would reject the Nat in the example you gave but would happily accept Constraint. So, this check does appear to be necessary.

testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs
23

I've fixed this. It had been failed because I had passed Nothing to kcConDecl somewhere.

andrewthad updated the Trac tickets for this revision.Mon, Jan 7, 10:11 AM
goldfire added inline comments.Mon, Jan 7, 11:00 AM
compiler/typecheck/TcInstDcls.hs
692

The code you have here looks good, but I'm still curious about that other check. It probably shouldn't accept Constraint, and so it sounds like you're describing a bug somewhere (likely not quite related to your additions).

@andrewthad, you've added Trac #15883 as a related Trac ticket in the Diff description, but is there a corresponding test case for it? (I can't find one.)

andrewthad updated this revision to Diff 19266.Mon, Jan 7, 3:31 PM
andrewthad marked an inline comment as done.
  • add two tests to confirm that 15883 is resolved

Good catch. I've added T15883 and UnliftedNewtypesForall to confirm that trac ticket Trac #15883 is resolved.

andrewthad updated this revision to Diff 19267.Wed, Jan 9, 10:17 AM
  • specify the impact of UnliftedNewtypes on CUSKs in the users manual
  • improve some of the typechecking code. remove some unneeded imports. all a data for data families that have a type family in the result kind.
andrewthad marked 10 inline comments as done.Wed, Jan 9, 10:44 AM

I've clarified the effect of UnliftedNewtypes on CUSK determination in the user guide. I've cleaned up the typechecking code some, implementing some of Richard's suggestions. I've added a test UnliftedNewtypesDifficultUnification, which currently fails with a panic. We get a different (and likely more meaningful) panic when we remove the last line of this test. With the last line removed, we have:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnliftedNewtypes #-}
module UnliftedNewtypesDifficultUnification where
import GHC.Exts
data Color = Red | Blue
type family Interpret (x :: Color) :: RuntimeRep where
  Interpret 'Red = 'IntRep
  Interpret 'Blue = 'WordRep
data family Foo (x :: Color) :: TYPE (Interpret x)

GHC panics with:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.7.20190109 for x86_64-unknown-linux):
       mkTyConKindRepBinds(TyConApp)
  Interpret
  Interpret x_av7[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:<line>:<column> in <package-id>:Outputable
        pprPanic, called at compiler/typecheck/TcTypeable.hs:<line>:<column> in <package-id>:TcTypeable

The relevant code from TcTypeable is:

new_kind_rep k@(TyConApp tc tys)                                               
  | Just rep_name <- tyConRepName_maybe tc                                     
  = do rep_id <- liftTc $ lookupId rep_name
       tys' <- mapM (getKindRep stuff in_scope) tys
       return $ nlHsDataCon kindRepTyConAppDataCon
                `nlHsApp` nlHsVar rep_id
                `nlHsApp` mkList (mkTyConTy kindRepTyCon) tys'
  | otherwise
  = pprPanic "mkTyConKindRepBinds(TyConApp)" (ppr tc $$ ppr k)

I'll keep investigating this, but if anyone's got any insights on this, I welcome them.

On an unrelated note, I am planning on unifying coerce and coerce#. The type signature of coerce, using the syntax from the Explicit Specificity Proposal will be:

coerce :: forall {r :: RuntimeRep} (a :: TYPE r) (b :: TYPE r). a -> b

This will simplify the code (we will not need to do any magic with rewrite rules) and allows users to use type applications in a natural way. Let me know if there are any objections to this.

compiler/typecheck/TcTyClsDecls.hs
1110

I've implemented this (although I just realized that I forgot to prompt the user to open a feature request in the error). I've introduced a test UnliftedNewtypesDifficultUnification to confirm that this works, but sadly, it panics for an unrelated reason. I have more information about this in a top-level comment.

1637

I should still investigate where else this is getting checked.

3227

Unfortunately, isLiftedType_maybe can *also* panic. This only happens when the kind does not have the form TYPE r. I may need to concoct a safer version of isLiftedType_maybe for this.

That mkTyConKindRepBinds panic is bizarre. This suggests that GHC is trying to create Typeable bindings for the kind of Foo. But Typeable doesn't support type families (like Interpret), so it shouldn't be attempting to create those bindings in the first place! Perhaps the issue is GHC simply not recognizing this fact. (I've observed similar issues here, although I haven't managed to get that exact mkTyConKindRepBinds panic before.)

andrewthad marked an inline comment as done.Wed, Jan 9, 11:16 AM

It gets worse! We can get the same exact problem without any data families. Behold:

{-# LANGUAGE DataKinds #-}                                                     
{-# LANGUAGE GADTSyntax #-}                                                    
{-# LANGUAGE MagicHash #-}                                                     
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}                                                  
{-# LANGUAGE UnliftedNewtypes #-}
                                                                               
module Unknown where                                                           
                                                                               
import GHC.Exts
                                                                               
data Color = Red | Blue
  
type family ToRuntimeRep (x :: Color) :: RuntimeRep where                      
  ToRuntimeRep 'Red = 'IntRep                                                  
  ToRuntimeRep 'Blue = 'WordRep
                                                                               
type family ToType (x :: Color) :: TYPE (ToRuntimeRep x) where                 
  ToType 'Red = Int#
  ToType 'Blue = Word#

newtype Foo (x :: Color) :: TYPE (ToRuntimeRep x) where
  FooC :: forall (x :: Color). ToType x -> Foo x

This produces the same exact panic. So maybe, as Ryan suggests, the code for Typeable doesn't like having a type family in the result kind? It was previously impossible for this to happen since the only way for a type family to show up in a result kind was if the declaration in question was itself a type family (which doesn't get a derived Typeable instance).

The Typeable related panic shouldn't be hard to stop. I'm not sure offhand where the fix is (there already have to be a slew of checks before generating Typeable instances), but it sounds like Ryan knows. If you can't find it, ask and I'll take a closer look.

compiler/typecheck/TcTyClsDecls.hs
3227

No -- I think you'll be OK calling isLiftedType_maybe here. If the kind of that type doesn't have form TYPE r, we really should panic.

but it sounds like Ryan knows.

On the contrary, I haven't the slightest clue how to fix this! This is why Trac #15862 is still an open issue :)

The only check I see in TcTypeable.hs to figure out what to generate Typeable bindings for is needs_typeable_binds. But that cannot be the full picture. Totday, GHC already correctly rejects:

import GHC.Exts
import Data.Kind
import Type.Reflection
import Data.Proxy

data Color = Red | Blue | Green

data SingColor :: Color -> Type where
  SingRed :: SingColor 'Red
  SingBlue :: SingColor 'Blue
  SingGreen :: SingColor 'Green

type family ToRuntimeRep (x :: Color) :: RuntimeRep where
  ToRuntimeRep 'Red = 'IntRep
  ToRuntimeRep 'Blue = 'WordRep
  ToRuntimeRep 'Green = 'LiftedRep

data Foo :: forall (x :: Color). SingColor x -> TYPE (ToRuntimeRep x) -> Type where

ex1 :: TypeRep (Foo SingRed)
ex1 = typeRep

I don't see where the other checks are happening that cut down on what things get typeable bindings generated.

Nevermind, it looks like there's some additional filtering that happens in todoForTyCons. I'll keep looking.

andrewthad updated this revision to Diff 19269.Wed, Jan 9, 4:06 PM
  • improve some of the typechecking code. remove some unneeded imports. all a data for data families that have a type family in the result kind.

I've fixed the panic coming from the typeable machinery. But there's another panic that is more difficult to track down. If I use GADT syntax to provide a kind signature in UnliftedNewtypesDifficultUnification, I get the error I expect:

newtype instance Foo 'Red :: TYPE (Interpret 'Red) where                        
  FooRedC :: Int# -> Foo 'Red

This fails as it should (since we don't know what to do with the coercion). This one also fails:

newtype instance Foo 'Red :: TYPE 'IntRep where                        
  FooRedC :: Int# -> Foo 'Red

Although the error message is subpar. But this one panics:

newtype instance Foo 'Red = FooRedC Int#

I've found that the panic happens when we go into: tcDataFamInstDecl > checkValidTyCon > checkValidDataCon > checkValidType. The worst part is that -ddump-tc-trace hangs somewhere, so I cannot get any debug output about what's going wrong. But the only difference between the code path that causes a panic and the one that doesn't is that the non-panicing one passes a kind signature to tc_kind_sig and the panicing one doesn't.

Yes, -ddump-tc-trace sometimes hangs. My approach there is to add a bunch more traces (printing out strings only) to learn where the hang is. Then, you'll find some knot-tied something being printed out. Remove the printing. This is a bug that you have the opportunity to find and fix. :)

Are you stuck looking for the panic? Time is short (as always), but I can take a look if you're stuck.

Ah, I had assumed the loop while tracing was something I had done, but you're right that it was already present. I found the bad trace statement and removed it. I figured out where this panic is happening, but I don't understand how to stop it. At some point during typechecking, we call checkUserTypeError on the data constructor. Here it is with some extra trace statements I've added:

checkUserTypeError = check 
  where
  check ty = traceTc "checkUserTypeError step" (ppr ty) >> traceTc "checkUserTypeError filler" (text "uht") >> step ty
  step ty
    | Just msg     <- userTypeError_maybe ty  = traceTc "checkUserTypeError guard A" (text "hutone") >> fail_with msg
    | Just (_,ts)  <- splitTyConApp_maybe ty  = traceTc "checkUserTypeError guard B" (vcat (map ppr ts)) >> mapM_ check ts
    | Just (t1,t2) <- splitAppTy_maybe ty     = traceTc "checkUserTypeError guard C" (vcat [ppr t1, ppr t2]) >> check t1 >> check t2
    | Just (_,t1)  <- splitForAllTy_maybe ty  = traceTc "checkUserTypeError guard D" (text "hutone") >> check t1
    | otherwise                               = return ()

Here's the code we are typechecking:

data Color = Red | Blue                                                            
type family Interpret (x :: Color) :: RuntimeRep where
  Interpret 'Red = 'IntRep
  Interpret 'Blue = 'WordRep
data family Foo (x :: Color) :: TYPE (Interpret x)                                 
newtype instance Foo 'Red = FooRedC Int#

And here's the relevant trace:

checkValidDataCon
  FooRedC
  UnliftedNewtypesDifficultUnification.R:Foo
  []
  Foo :: forall (x :: Color) -> TYPE (Interpret x)
  Foo :: forall (x :: Color) -> TYPE (Interpret x)
checkValidDataCon 2 Int# -> Foo
checkValidType Int# -> Foo :: *
checkValidType bar here hutone
checkUserTypeError step Int# -> Foo
checkUserTypeError filler uht
checkUserTypeError guard C
  (->) Int#
  Foo
checkUserTypeError step (->) Int#
checkUserTypeError filler uht
checkUserTypeError guard B

This actually crashes while printing the trace since the trace, but even without the trace it still panics (just a hair later). What happens is that GHC is doing a validity check on the type of FooRedC. For reasons I don't understand, the result type for data instance constructors is unsaturated. That is, the data constructor has type Int# -> Foo and not type Int# -> Foo 'Red. I don't understand why this is the case, but I'm guessing there are good reasons for it. The recursive step inside checkUserTypeError pulls apart Int# -> Foo into (->) Int# and Foo with splitAppTy_maybe. That's where things go wrong. Because of this:

repSplitAppTy_maybe (FunTy ty1 ty2)
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
  where
    rep1 = getRuntimeRep ty1
    rep2 = getRuntimeRep ty2

Getting the runtime rep of Foo causes a panic, although I'm not sure why.

That is, the data constructor has type Int# -> Foo and not type Int# -> Foo 'Red. I don't understand why this is the case, but I'm guessing there are good reasons for it.

There are no good reasons for it. Forget about unsaturated: that's ill-kinded. And it's why the panic happens. You're hot on the enemy's trail here -- keep marching forward! :)

Ah, that's good to know. I've now gotten to the bottom (or very close to the bottom) of it. Over in tcDataFamHeader, unravelFamInstPats was misbehaving. But, it only misbehaves because it's receiving a bad type:

(Foo 'Red |> (TYPE (UnliftedNewtypesDifficultUnification.D:R:Interpret[0]))_N)

Yikes. Why is there an unsolved variable in there? Let's move look further up in tcDataFamHeader (with some trace statements added):

tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt
                hs_pats m_ksig hs_cons new_or_data
  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind)))
            <- pushTcLevelM_                                $
               solveEqualities                              $
               bindImplicitTKBndrs_Q_Skol imp_vars          $
               bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
               do { stupid_theta <- tcHsContext hs_ctxt
                  ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
                  ; traceTc "tcDataFamHeader lhs_ty 1:" (ppr lhs_ty)
                  ; res_kind <- tc_kind_sig m_ksig
                  ; traceTc "tcDataFamHeader lhs_kind:" (ppr lhs_kind)
                  ; traceTc "tcDataFamHeader res_kind:" (ppr res_kind)
                  ; mapM_ (wrapLocM_ (kcConDecl new_or_data res_kind)) hs_cons
                  ; lhs_ty <- checkExpectedKindX pp_lhs lhs_ty lhs_kind res_kind
                  ; traceTc "tcDataFamHeader lhs_ty 2:" (ppr lhs_ty)
                  ; return (stupid_theta, lhs_ty, res_kind) }

Let's see what these extra traces show:

tcDataFamHeader lhs_ty 1: Foo 'Red
newAnonMetaTyVar t_a10U[tau:1]
tcDataFamHeader lhs_kind: TYPE (Interpret 'Red)
tcDataFamHeader res_kind: TYPE t_a10U[tau:1]
...
tcDataFamHeader lhs_ty 2: (Foo 'Red |> (TYPE {co_a10W})_N)

Oh no! The call to checkExpectedKindX regresses lhs_ty. Later co_a10W becomes (UnliftedNewtypesDifficultUnification.D:R:Interpret[0])), but we are still stuck with a variable that we cannot solve. And this absolutely makes sense. Type families are not injective. From here, we cannot figure out what the argument to Interpret should be. We only know that Interpret[0] ~ 'IntRep.

The only fix I can think of it to revert the use of newOpenTypeKind in tc_kind_sig. If I go back to just feeding in lhs_kind, I can avoid creating an unsolvable variable. Maybe there's a better way though. @goldfire Any recommendations?

I've confirmed that the fix I suggested does work. But I feel like the other solution (inventing a metavar) should work too. I analyzed it wrong above. In particular, UnliftedNewtypesDifficultUnification.D:R:Interpret[0] is a coercion. Here's where I think the real problem may be:

checkExpectedKind
  Foo 'Red
  act_kind: TYPE (Interpret 'Red)
  act_kind': TYPE (Interpret 'Red)
  exp_kind: TYPE t_a10U[tau:1]
...
New coercion hole: co_a10W
utype_defer
  Interpret 'Red
  'IntRep
  arising from a type equality TYPE (Interpret 'Red)
                               ~
                               TYPE t_a10U[tau:1]

...
matchFamTcM
  Matching: Interpret 'Red
  Match succeeded:
    Rewrites to: 'IntRep
    Coercion: UnliftedNewtypesDifficultUnification.D:R:Interpret[0]
...
tcDataFamHeader 1
  (Foo 'Red |> (TYPE
                  (UnliftedNewtypesDifficultUnification.D:R:Interpret[0]))_N)

And that last bit is what makes unravelFamInstPats give wrong output. What I'm wondering is whether or not it's right to build this coercion. I don't think it is. I think Interpret 'Red should be reduced to 'IntRep very early on in tcDataFamHeader. But I'm not sure.

Hmmm... in tcDataFamHeader's doppelganger, tcTyFamInstEqnGuts, we find this telling comment:

; let pats = unravelFamInstPats lhs_ty                                      
      -- Note that we do this after solveEqualities                         
      -- so that any strange coercions inside lhs_ty                        
      -- have been solved before we attempt to unravel it

But solveEqualities does not appear to have solved our strange coercion.

Wait a second. What's this?!:

unravelFamInstPats fam_app                                                         
  = case splitTyConApp_maybe fam_app of                                            
      Just (_, pats) -> pats                                                       
      Nothing        -> WARN( True, bad_lhs fam_app ) []                           
        -- The Nothing case cannot happen for type families, because               
        -- we don't call unravelFamInstPats until we've solved the                 
        -- equalities.  For data families I wasn't quite as convinced              
        -- so I've let it as a warning rather than a panic.

I'm not sure how WARN gets handled by the compiler, but my suspicion is that the warning is silently discarded. So the question is, what's the right thing to do here?

  • make unravelFamInstPats accept a type with a cast. remove a trace statement that caused the compiler to hang.
andrewthad updated this revision to Diff 19271.Fri, Jan 11, 2:11 PM
  • Collapsed coerce# and coerce back into one function. Make sure all typechecker tests pass.
andrewthad updated this revision to Diff 19272.Fri, Jan 11, 2:13 PM
andrewthad marked an inline comment as done.
  • remove coerceLiftedKey
andrewthad updated this revision to Diff 19273.Fri, Jan 11, 2:21 PM
  • add test for VTA on coerce

Let's take a step back:

The UnliftedNewtypesDifficultUnification test is meant not to be compiled, right? The idea is that this is an example of the case that's beyond GHC's ability to handle right now. This is to be caught in kcConDecl. And the trouble you're getting is from the call to unravelFamInstPats later in kcConDecl. (By the way, WARNings are printed out only in compilers built with DEBUG enabled, by choosing, e.g., the devel2 settings in your build.mk file.) There is an easy answer here: have decideNewtypeKind fail if the coercion returned from unifyKind is non-reflexive. failWithTc is a good way to do this. Then, we can be assured we never proceed in the troublesome case.

Does that make sense?

andrewthad marked 17 inline comments as done.Fri, Jan 11, 3:24 PM

I've made coerce and coerce# the same function. All comments about documentation of coerce# and about the rewrite rules stuff are now moot, so I have marked them complete. All tests now pass. I still need to do a few documentation things. Could @goldfire or @simonpj confirm that what I have done in unravelFamInstPats is sound?

compiler/typecheck/TcInstDcls.hs
692

I realized that UnliftedNewtypesFamilyKindFail2 doesn't actually have a doubled error message. It has two error messages, and they are both meaningful. I think I was incorrect earlier when I said that there was another check that rejected Nat but accepted Constraint.

809–810

This is done now. And the example code you gave has been pulled into UnliftedNewtypesUnassociatedFamily, which passes.

testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr
2

Surprisingly, this error message has become better, although it is somewhat by accident. I think became better as a result of two things:

  • Less omitted checks.
  • Not throwing away the coercion you were concerned about discarding.

I'm guessing that the kind ends up as something like TYPE (a0 |> co1), and the cast gets shot down immediately.

No, I don't think the new implementation of unravelFamInstPats is good: throwing away the cast might cause trouble later on. I still say we shouldn't ever see the case with the coercion, because kcConDecl won't let us. My guess is that you didn't see my earlier comment before posting yours.

andrewthad marked 2 inline comments as done.Fri, Jan 11, 3:48 PM

Sorry, I just now saw your comment Richard. I had already made the appropriate change to kcConDecl, but that turned out to not be enough. To see why, consider the trace output I was looking at earlier:

tcDataFamHeader lhs_kind: TYPE (Interpret 'Red)
tcDataFamHeader res_kind: TYPE t_a10U[tau:1]

The lhs_kind and the res_kind as we are working our way through:

do { stupid_theta <- tcHsContext hs_ctxt                            
   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats    
   ; res_kind <- tc_kind_sig m_ksig                                 
   ; mapM_ (wrapLocM_ (kcConDecl new_or_data res_kind)) hs_cons     
   ; lhs_ty <- checkExpectedKindX pp_lhs lhs_ty lhs_kind res_kind   
   ; return (stupid_theta, lhs_ty, res_kind) }

The weakness is that kcConDecl calls decideNewtypeKind, where unifyKind happily produces a reflexive coercion involving t_a10U[tau:1]. If we passed lhs_kind into kcConDecl instead of res_kind, this wouldn't happen. (That's the benefit of the "don't invent a fresh metavar" approach). So, I worked an extra case into unravelFamInstPats to make it accept a cast. What's strange about what I've done is that now GHC will actually accept the instance if you omit the kind signature, but it rejects it if you include the signature (using GADT syntax on the instance). I'm not sure if this is a bad thing. The only alternative I see to changing unravelFamInstPats is going back to threading lhs_kind through instead of inventing a metavar. That would lead to a failure regardless of whether or not a kind signature was provided.

As a minor aside, I feel that the fall-through case in unravelFamInstPats should be a panic and not a WARN. Returning an empty list as the arguments is almost certain to cause a panic elsewhere, and I think it's preferable to get the panic at the place something went wrong.

And I just missed that one as well. Sorry, my previous comment was in response to the one before your last one, not your last one.

simonpj added a comment.EditedWed, Jan 16, 6:11 AM

I'm not sure how WARN gets handled by the compiler, but my suspicion is that the warning is silently discarded. So the question is, what's the right thing to do here?

I'm not following all the details here; but I'm pretty definite that this branch of unravelFamInstPats should fail completely, with some (probably hard to understand) error message.

See Trac Trac #15905 comment:11

libraries/ghc-prim/GHC/Types.hs
285

I agree with Richard: we should make the source code match the wired-in type. So yes, explicit kind variables.