Unnecessarily complicated left-hand side for SPECIALIZE pragma causing RULE left-hand side too complicated to desugar

GHC 7.10.2 rejects the SPECIALIZE pragma in the following snippet with "RULE left-hand side too complicated to desugar".

class C a where
  type TF a; m :: a -> TF a

instance C Int where
  type TF Int = String; m = show

overloaded :: C a => a -> (a,TF a)
{-# INLINABLE overloaded #-}
overloaded a = (a,m a)

{-# SPECIALIZE overloaded :: Int -> (Int,TF Int) #-}

This use case is so simple/basic/prevalent that it seems inappropriate to reject it.

The actual message is

    RULE left-hand side too complicated to desugar
      Optimised lhs: case cobox_awc
                     of _ [Occ=Dead] { GHC.Types.Eq# cobox ->
                     overloaded @ Int $dC_awb
                     }
      Orig lhs: case cobox_awc of cobox_awc { GHC.Types.Eq# cobox ->
                overloaded @ Int $dC_awb
                }

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#10555
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

I'm unfamiliar with the implementation of the type-checker. Even so, I flipped on -ddump-tc-trace to investigate where that troublesome coercion was coming from. I noticed the following subsequence of trace messages.

tcSubTypeDS_NC
  the type signature for ‘overloaded’
  a_awb[tau:1] -> (a_awb[tau:1], TF a_awb[tau:1])
  Int -> (Int, TF Int)
*snip*
writeMetaTyVar a_awb[tau:1] := Int
*snip*
utype_defer
  cobox_awd
  TF a_awb[tau:1]
  TF Int
  arising from a type equality a_awb[tau:1]
                               -> (a_awb[tau:1], TF a_awb[tau:1])
                               ~
                               Int -> (Int, TF Int)
*snip*
u_tys yields coercion: cobox_awd

This indicates that cobox_awd (the primary part of cobox_awc) is the result of the unifier deferring the question of whether TF a_awb ~ TF Int, even though a_awb was already set to Int.

Digging a bit deeper, I see that TcUnify.uType contains the following matches, which ultimately incur the coercion that sinks the SPECIALISE pragma since they do not check if the types' already solved tyvars admit reflexivity as a proof here.

        -- Always defer if a type synonym family (type function)
        -- is involved.  (Data families behave rigidly.)
    go ty1@(TyConApp tc1 _) ty2
      | isTypeFamilyTyCon tc1 = uType_defer origin ty1 ty2
    go ty1 ty2@(TyConApp tc2 _)
      | isTypeFamilyTyCon tc2 = uType_defer origin ty1 ty2

I anticipate that a possible "fix" for this ticket would be for the go function to check if the solved type variables render ty1 and ty2 equivalent such that TcRefl would suffice here. Or perhaps there's somewhere more appropriate (dsSpec?) to perform that "optimization" for the sake of accepting SPECIALIZE pragmas like this one.

The proposal in #12649 might involve an "alternate" code path in the type-checker that side-steps this issue: if a SPECIALIZE pragma could be declared more directly ("set a to Int"), then decomposeRuleLhs (the function that emits "RULE left-hand side too complicated to desugar") might not even be necessary.

changed title from unnecessarily complicated left-hand side causing RULE left-hand side too complicated to desugar to Unnecessarily complicated left-hand side for SPECIALIZE pragma causing RULE left-hand side too complicated to desugar

closed

Closing this ticket -- the SPECIALIZE pragma is accepted and works as expected in in GHC 8.0.1.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWorksForMe

mentioned in commit c469db4e

Trac metadata

Trac field	Value
Test case	- → deSugar/should_compile/T12950

added error messages label

added Pnormal label