Re: [GHC] #14059: COMPLETE sets don't work at all with data family instances

30 May 2018

      #14059: COMPLETE sets don't work at all with data family instances
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms,
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 OK, I at least know why the error messages are different in GHC 8.4. It's
 due to the fix for #14135, which filters out candidate conlikes from
 `COMPLETE` sets with
 [http://git.haskell.org/ghc.git/blob/857005a762a12e021c3cc65b729bd6263b7145fb...
 this criterion]:

 {{{#!hs
       isValidCompleteMatch :: Type -> [ConLike] -> Bool
       isValidCompleteMatch ty =
         isJust . mapM (flip tcMatchTy ty . resTy . conLikeFullSig)
         where
           resTy (_, _, _, _, _, _, res_ty) = res_ty
 }}}

 I believe this criterion is too conservative, since it requires the type
 of every conlike in a `COMPLETE` set to match the type of the scrutinee.
 But that assumption doesn't hold true when one of the conlikes is for a
 GADT constructor, as in the second example from the description:

 {{{#!hs
 data SBool (z :: Bool) where
   SFalse :: SBool False
   STrue  :: SBool True

 pattern STooGoodToBeTrue :: forall (z :: Bool). ()
                          => z ~ True
                          => SBool z
 pattern STooGoodToBeTrue = STrue
 {-# COMPLETE SFalse, STooGoodToBeTrue #-}

 wobble :: SBool z -> Bool
 wobble STooGoodToBeTrue = True
 }}}

 Here, the type of the scrutinee in `wobble` is `SBool z`, but the type of
 the first conlike in the `COMPLETE` set is `SBool False`, so `tcMatchTy
 (SBool False) (SBool z)` will return `Nothing`, which means we filter out
 that `COMPLETE` set entirely. This is terrible, since `SFalse` //can// be
 pattern-matched on in `wobble`!

 This leads me to believe that we should only be performing this
 `tcMatchTy` check on pattern synonym constructors, not data constructors.
 I applied this change to `isValidCompleteMatch` locally and sure enough,
 the error message in this ticket went back to what is was in 8.2. I'll
 prepare a patch with this payload before investigating the underlying
 issue in this ticket further.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14059#comment:7
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler