[GHC] #14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull)

[GHC]

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  carlostome
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.3
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by carlostome):

 I've found that this error is caused by the order of the arguments to
 `tcMatchTy` in the following code.

 {{{
 mkOneConFull x con = do
   let res_ty  = idType x
       (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys,
 con_res_ty)
         = conLikeFullSig con
       tc_args = tyConAppArgs res_ty
       subst1  = case con of
                   RealDataCon {} -> zipTvSubst univ_tvs tc_args
                   PatSynCon {}   -> expectJust "mkOneConFull" (tcMatchTy
 con_res_ty res_ty)
   ...
 }}}

 Adding some debugging information I noticed that the call that makes
 `tcMatchTy` return `Nothing` and therefore trigger the error it is done
 with the following arguments (as outputed with -dppr-debug):
 {{{
   con_res_ty = main:T14135.Foo{tc r9} ghc-prim:GHC.Types.Int{(w) tc 3u}
   res_ty     = main:T14135.Foo{tc r9} (a{tv aWz} [tv] :: *)
 }}}
 As far as I understand the problem stands because `tcMatchTy` expects the
 first argument to be a kind of template type that will get instantiated to
 match the second argument.
 However, it is clear that there is no substitution s such that s(Int) = a.

 If we change the call to `tcMatchTy res_ty con_res_ty` then the example
 program compiles fine but when trying to validate, ghc is not able to
 build anymore `Data.Typeable.Internal` because it triggers the exactly
 same error.

 I have found that by substituting `tcMatchTy` by `tcUnifyTy` we solve the
 full problem, however, I don't know if `tcMatchTy` should be prefered over
 `tcUnify` or not (if it makes a semantic difference).

 Any insight on this?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14135#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler