tcInferRho muddies the waters

In trying to understand the algorithm implemented in !TcExpr, I've spent some time examining tcInferRho. I conjecture that this function is superfluous and should be removed, in favor of tcInfer . tcExpr. Some of these thoughts were first written up in this thread.

After a considerable amount of staring, I've actually found a misbehavior caused by the current implementation. tcInferRho calls tcInfExpr, which has only 3 special cases before calling tcInfer . tcExpr: for variables, parentheses, and application. I was first drawn into this problem because these three cases seem woefully insufficient for the problem at hand. I was surprised how such a paucity of cases could have survived without causing havoc, if indeed tcInferRho were necessary at all. For example, only normal (prefix) application is handled; infix application is missing.

In looking at differences between tcInferApp (which is called from the application case of tcInfExpr) and tcApp (called from tcExpr), I saw that the former doesn't have a special case for seq while the latter does. And, indeed, this difference is exploitable.

This compiles fine:

foo _ = case () `seq` (# #) of (# #) -> ()

This does not:

foo _ = case seq () (# #) of (# #) -> ()

which produces

Scratch.hs:15:21:
    Kind incompatibility when matching types:
      b0 :: *
      (# #) :: #
    In the second argument of ‘seq’, namely ‘(##)’
    In the expression: seq () (##)

Looking at the code, this behavior is expected, because the first version of the code calls into tcInfer . tcExpr, which special-cases seq, while the second is caught by tcInferApp, which doesn't have the special case. The above example shows that this isn't just a theoretical concern about code cleanup!

This all leads to another question: Why special-case seq at all? !MkId tells me that

seq :: forall (a :: *) (b :: *). a -> b -> b

Why isn't it

seq :: forall (a :: *) (b :: OpenKind). a -> b -> b

With the second type, I would imagine that seq wouldn't need a special case in the type-checker. Is there something wrong with the second type for seq?

I'll post more thoughts to this ticket as I continue to explore.

Trac metadata

Trac field	Value
Version	7.9
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #7220 (closed)

changed weight to 5

added Tbug Trac import labels

I've tried removing tcInfExpr, in favor of having tcInferRhoNC call tcExpr directly. I'll post here once I see how it goes. I didn't find other special cases worth mentioning.

The situation with tcInfer etc is still not cool, but other things being equal simpler is definitely better. So I happy with your simplification.

Re seq, it's not quite so simple. We do NOT want seq 4 to have type Int# -> Int. E.g. this would be bad:

flob :: (Double# -> Bool) -> Bool
flob f = f 3.0##

bad = flob (seq True)

Why? Because bad would pass a partial application to flob, and flob would pass an Double# to seq; but seq is expecting a pointer as its first argument!

So it is really only saturated applications of seq that can be typed in this more flexible way; and those saturated applications are then recognised by the desugarer and turned into case expressions.

That said, it should work for prefix applications too, I agree. Maybe you could arrange for that, and add a Note with the above explanation?

Thanks

Simon

Ah, yes, that makes good sense. Patch will arrive soon. Thanks for the explanation.

This is subtler than I thought. The email trail linked in the original description suggests that TauTvs can be unified with forall-types, but cannot be solved to become a forall-type. This is true, but only partially: the forall-type in question must be devoid of any type families, *and* the TauTv must be of kind OpenKind.

I have implemented, in a branch here, a version of GHC missing tcInfExpr, the under-implemented version of tcExpr that infers a type instead of checking it. The problem is that, in that branch, the following fails:

{-# LANGUAGE RankNTypes, TypeFamilies #-}

module Rank where

type family ListTF x where
  ListTF x = [x]

bar :: (forall x. ListTF x -> Int) -> ()
bar _ = ()

foo = bar $ length

For the curious, the error message is

    Couldn't match type ‘[a0] -> Int’ with ‘forall x. ListTF x -> Int’
    Expected type: ([a0] -> Int) -> ()
      Actual type: (forall x. ListTF x -> Int) -> ()
    In the expression: bar
    In the expression: bar $ length

So, the "obvious" fix to the original bug doesn't work.

The problem outlined in this comment (interaction between the mention of type families and inference) can be observed in 7.8, with the following rather contrived construction:

{-# LANGUAGE RankNTypes, TypeFamilies #-}

module Rank where

type family ListTF x where
  ListTF x = [x]

bar :: (forall x. ListTF x -> Int) -> ()
bar _ = ()

myconst :: ((forall r. ListTF r -> Int) -> ()) -> x -> (forall r. ListTF r -> Int) -> ()
myconst x _ = x

foo = (bar `myconst` ()) $ length

If, in the last line, myconst is applied prefix instead of infix, the module compiles.

It seems the solution here is to fully implement tcInfExpr, instead of eliminate it, so that tcInfExpr is aware of infix operators, sections, and probably other expression forms. With that done, the problems outlined here should go away.

But, given the smelliness around all of this, I think it's best to let The Expert (who is on holiday, I understand) weigh in before proceeding. It's also worth noting that the problems I've encountered to post this ticket have all been "white box" -- I detected the problem reading GHC source code, not by stumbling into it. It's quite possible that this infelicity has never triggered a problem in the wild.

A discussion with various Experts revealed the following story:

GHC has a PolyTv flavor of meta-variable that, according to its description, is meant to unify with sigma-types. But, the original intent was more than that: it should unify with anything, always.

We sometimes want tcExpr to check a type, and we sometimes want it to infer a type. We can imagine two functions like this: (indeed, we have two functions like this!)

tcInfExpr :: HsExpr Name -> TcM (HsExpr TcId, TcType)
tcExpr :: HsExpr Name -> TcType -> TcM (HsExpr TcId)

If both of these were fully implemented, they would each have many similar cases and would be more work to maintain. This is why tcInfExpr currently has just a few cases and then delegates to tcExpr, passing in a unification variable. The problem is that the unification variable, currently a TauTv, won't unify with all types.

What we want, in effect, is this:

data TcDirection = Infer (Ref TcType) | Check TcType
tcExpr :: TcDirection -> HsExpr Name -> TcM (HsExpr TcId)

But, if we had a unification variable that unifies with anything, then we have exactly that: the permissive unification variable is essentially a Ref TcType!

We can use a PolyTv as this permissive unification variable. The only place where PolyTv is currently used is in the special typing rule for ($) (and its presence there is suspect -- see below). So, all we have to do is update checkTauTvUpdate to not check PolyTvs at all, and we get this behavior for PolyTv.

So, the current proposed solution is to get rid of TcInfExpr (as already done in my branch) and instead use a PolyTv in tcInfer, along with liberalizing the meaning of PolyTv.

To make sure we've done this right, we should also verify that PolyTvs are indeed filled in right away, before the constraint solver. In particular:

• Zonking (even the partial zonking done by zonkTcType and friends) should never encounter a Flexi PolyTv. (Nagging worry about the possibility of underspecified types here.... may need defaulting.)
• The constraint solver should never encounter a PolyTv.

About ($): There is a curious piece of code here:

tcExpr (OpApp arg1 op fix arg2) res_ty
  | (L loc (HsVar op_name)) <- op
  , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
  = do { traceTc "Application rule" (ppr op)
       ; (arg1', arg1_ty) <- tcInferRho arg1

       ; let doc = ptext (sLit "The first argument of ($) takes")
       ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty
       ; a_ty <- newPolyFlexiTyVarTy
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)

       ; co_a   <- unifyType arg2_ty   a_ty      -- arg2 ~ a
       ; co_b   <- unifyType op_res_ty res_ty    -- op_res ~ res
       ; op_id  <- tcLookupId op_name

       ; let op' = L loc (HsWrap (mkWpTyApps [a_ty, res_ty]) (HsVar op_id))
       ; return $
         OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $
                mkLHsWrapCo co_arg1 arg1')
               op' fix
               (mkLHsWrapCo co_a arg2') }

My question is: why have a_ty at all? The type of the left-hand argument to ($) is properly captured in arg_ty, and I can't see a reason to then unify with the fresh a_ty. Does anyone have insight here?

Re the last question, here's the comment in HEAD

       -- Make sure that the argument type has kind '*'
       -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
       --    (which gives a seg fault)
       -- We do this by unifying with a MetaTv; but of course
       -- it must allow foralls in the type it unifies with (hence PolyTv)!
       --
       -- The result type can have any kind (Trac #8739),
       -- so we can just use res_ty

       -- ($) :: forall (a:*) (b:Open). (a->b) -> a -> b
       ; a_ty <- newPolyFlexibTyVarTy

Simon

Of course. How silly of me -- I saw that comment but somehow didn't realize it answered my question.

Trac metadata

Trac field	Value
Differential revisions	→ D469

mentioned in commit fe6a5171

mentioned in commit e6e45a1c

mentioned in commit 1e2002d8

Keeping ticket open. I merged my solution at Simon's request, but there's still an outstanding refactoring task. See D469.

Can you just lay out what the "refactoring task" is? Thanks

Simplifying the rule for ($), as you requested.

On D469, Simon says, about line 328 of !TcExpr:

This smells wrong. tcInferRho ends up calling tcInfer, which makes an OpenKind ReturnTv. But then we unify it with a liftedTypeKind ReturnTv later.

Complicated and silly. Better if tcInferRho takes the kind it is expecting. Then we have only one ReturnTv, not two; and the whole ReturnTv story is located in tcInfer, rather than having a non-return-ish hack in the typing rule for $

Make sense?

I've decided: no, this doesn't make sense. The call to tcInferRho is to infer the type of the left-hand argument to $. This type is a function type arg -> res. If it turns out to be unlifted, the matchExpectedFunTys will fail. The silliness with the new ReturnTy bit isn't about the result of tcInferRho -- it's about the result of matchExpectedFunTys. So the straightforward refactoring Simon proposes doesn't work.

Instead, what we should do here is to unify arg2_ty's kind with *. But !TcUnify doesn't have a function for that -- something like matchExpectedStar. The closest thing -- unifyKindX -- tells us about sub-kinding relationships, instead of actually unifying the kinds.

So, I propose: do nothing for now. It's working, although a little uglily, as is. When we have proper kind equalities and no sub-kinding anymore, this will be easy to fix. Please close the ticket if you agree.

closed

Yes I agree.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label