Opened 3 years ago

Last modified 2 years ago

#13105 new bug

Allow type families in RuntimeReps

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: LevityPolymorphism Cc: magesh.b, vagarenko
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T13105
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Conal Elliott provided me with this puzzle:

type family RepRep a ∷ RuntimeRep

class HasRep a where
  type Rep a ∷ TYPE (RepRep a)
  repr ∷ a → Rep a
  abst ∷ Rep a → a

type instance RepRep Int = IntRep

instance HasRep Int where
  type Rep Int = Int#
  abst n = I# n
  repr (I# n) = n

I think we should accept. However, doing so (even with my solution to #12809 complete) is hard, because we frequently consult a kind in order to determine a runtime representation. When that kind is TYPE (RepRep Int), the code generator throws up its arms in despair.

The solution here is either to teach the code generator how to normalise types (requiring propagating the FamInstEnvs) or to do a whole-program transformation at some point (zonker? desugarer? maybe we can wait until CorePrep or even unarisation?) to change ids whose types have kinds like TYPE (RepRep Int) into ids with types with kinds like TYPE IntRep.

But I don't want to let this hold me up at the moment, so I'm posting here as a reminder to revisit this problem.

Change History (14)

comment:1 Changed 3 years ago by goldfire

Test Case: typecheck/should_fail/T13105

I've added a test case (in my work on #12809, at Phab:D2842), but it's a compile_fail test, just because code like this originally made my branch panic. It doesn't panic now, and I want to keep it that way until this bug is addressed properly.

Fixing this bug should make the test succeed.

comment:2 Changed 3 years ago by goldfire

Keywords: LevityPolymorphism added

comment:3 Changed 3 years ago by simonpj

When that kind is TYPE (RepRep Int), the code generator throws up its arms in despair.

So presumably the Lint check that every argument is not levity-polymorphic fails? Actually seeing the code fragment would be helpful.

Assuming it's a Lint failure (which I think it could be), can't the type checker just normalise before spitting out the argument code?

comment:4 Changed 3 years ago by goldfire

Yes, the levity-polymorphism check sees the problem and reports a type of kind TYPE (RepRep Int) as levity-polymorphic. I will have a note in the manual about this. If the type checker didn't catch it, it would be a lint error, yes.

I don't think it's as simple as a normalisation step in the type checker. For example:

foo :: forall (a :: TYPE (RepRep Int)). a -> a
foo x = x

In this code, x has type a. What's to normalise about that?? Now we could say that x :: a |> co where co :: TYPE (RepRep Int) ~ TYPE IntRep. But now x's type has changed and that means we need to use casts wherever x has been used. And this is an easy case where the type checker can see the correct, normalised type from the get-go. In general, unification and type family reduction may be necessary before we can proceed.

comment:5 Changed 3 years ago by simonpj

I was thinking of this as an adjunct to the LP test in the desugarer. If the argument of an application has type ty :: TYPE k, and k does not pass the LP test (yet), then normalise k (using top level instances only) and cast the arg wtih a coercion TYPE k ~ TYPE k_norm.

comment:6 Changed 3 years ago by goldfire

But that means the argument would change type from ty to ty |> co. Other bits of the expression might have to change, too.

comment:7 Changed 3 years ago by simonpj

Sure. Instead of f e we'd have f (e |> co). That's fine.

comment:8 Changed 3 years ago by goldfire

But if f e is well-typed, then f (e |> co) surely isn't. We would need (f |> co') (e |> co) or some such. I imagine this is what we'll have to do, but it doesn't seem trivial.

The other possibility may be to normalise types as we're converting to Stg, where types don't matter. This poses other challenges, in that the levity-polymorphism checks in the desugarer and in Core Lint will have to distinguish between type family applications that can reduce and those that can't. Might be easier than the program transformation, though.

comment:9 Changed 3 years ago by Richard Eisenberg <rae@…>

In e7985ed2/ghc:

Update levity polymorphism

This commit implements the proposal in
https://github.com/ghc-proposals/ghc-proposals/pull/29 and
https://github.com/ghc-proposals/ghc-proposals/pull/35.

Here are some of the pieces of that proposal:

* Some of RuntimeRep's constructors have been shortened.

* TupleRep and SumRep are now parameterized over a list of RuntimeReps.
* This
means that two types with the same kind surely have the same
representation.
Previously, all unboxed tuples had the same kind, and thus the fact
above was
false.

* RepType.typePrimRep and friends now return a *list* of PrimReps. These
functions can now work successfully on unboxed tuples. This change is
necessary because we allow abstraction over unboxed tuple types and so
cannot
always handle unboxed tuples specially as we did before.

* We sometimes have to create an Id from a PrimRep. I thus split PtrRep
* into
LiftedRep and UnliftedRep, so that the created Ids have the right
strictness.

* The RepType.RepType type was removed, as it didn't seem to help with
* much.

* The RepType.repType function is also removed, in favor of typePrimRep.

* I have waffled a good deal on whether or not to keep VoidRep in
TyCon.PrimRep. In the end, I decided to keep it there. PrimRep is *not*
represented in RuntimeRep, and typePrimRep will never return a list
including
VoidRep. But it's handy to have in, e.g., ByteCodeGen and friends. I can
imagine another design choice where we have a PrimRepV type that is
PrimRep
with an extra constructor. That seemed to be a heavier design, though,
and I'm
not sure what the benefit would be.

* The last, unused vestiges of # (unliftedTypeKind) have been removed.

* There were several pretty-printing bugs that this change exposed;
* these are fixed.

* We previously checked for levity polymorphism in the types of binders.
* But we
also must exclude levity polymorphism in function arguments. This is
hard to check
for, requiring a good deal of care in the desugarer. See Note [Levity
polymorphism
checking] in DsMonad.

* In order to efficiently check for levity polymorphism in functions, it
* was necessary
to add a new bit of IdInfo. See Note [Levity info] in IdInfo.

* It is now safe for unlifted types to be unsaturated in Core. Core Lint
* is updated
accordingly.

* We can only know strictness after zonking, so several checks around
* strictness
in the type-checker (checkStrictBinds, the check for unlifted variables
under a ~
pattern) have been moved to the desugarer.

* Along the way, I improved the treatment of unlifted vs. banged
* bindings. See
Note [Strict binds checks] in DsBinds and #13075.

* Now that we print type-checked source, we must be careful to print
* ConLikes correctly.
This is facilitated by a new HsConLikeOut constructor to HsExpr.
Particularly troublesome
are unlifted pattern synonyms that get an extra void# argument.

* Includes a submodule update for haddock, getting rid of #.

* New testcases:
  typecheck/should_fail/StrictBinds
  typecheck/should_fail/T12973
  typecheck/should_run/StrictPats
  typecheck/should_run/T12809
  typecheck/should_fail/T13105
  patsyn/should_fail/UnliftedPSBind
  typecheck/should_fail/LevPolyBounded
  typecheck/should_compile/T12987
  typecheck/should_compile/T11736

* Fixed tickets:
  #12809
  #12973
  #11736
  #13075
  #12987

* This also adds a test case for #13105. This test case is
* "compile_fail" and
succeeds, because I want the testsuite to monitor the error message.
When #13105 is fixed, the test case will compile cleanly.

comment:10 Changed 3 years ago by goldfire

NB: The above commit does not fix this!

comment:11 Changed 2 years ago by magesh.b

Cc: magesh.b added

comment:12 Changed 2 years ago by magesh.b

class Unbox (t :: *) (r :: TYPE k) | t -> r, r -> t where
  unbox :: t -> r
  box :: r -> t
  
instance Unbox Int Int# where
  unbox (I# i) = i
  box i = I# i

instance Unbox Char Char# where
  unbox (C# c) = c
  box c = C# c

instance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where
  unbox (a,b) = (# unbox a, unbox b #)
  box (# a, b #) = (box a, box b)

-- Works fine
testInt :: Int
testInt = box (unbox 1)

-- Throws an error at call site
{-error:
• Couldn't match a lifted type with an unlifted type
      When matching the kind of ‘Int#’
    • In the expression: box (unbox (1, 'a'))
      In an equation for ‘testTup’: testTup = box (unbox (1, 'a'))
    |
168 | testTup = box (unbox (1, 'a'))
    |           ^^^^^^^^^^^^^^^^^^^^
-}


testTup :: (Int, Char)
testTup = box (unbox (1, 'a'))

Does this error related to same bug?

Any chance of such code to work in future GHC release or is it fundamentally not possible to have a levity polymorphic class as a constraint in an instance declaration.

One of the use case is, above code would have allowed me to pack user defined data type in to highly packed unboxed anonymous record (using nested Unboxed Tuple) making boxing/unboxing first class in GHC.

comment:13 Changed 2 years ago by vagarenko

Cc: vagarenko added

comment:14 Changed 2 years ago by goldfire

comment:12 seems unrelated, but is problematic. See #14185.

Note: See TracTickets for help on using tickets.