[GHC] #15685: Pattern signature not inferred

[GHC]

#15685: Pattern signature not inferred
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
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 simonpj):

 OK I see what is happening.

 * There really is an error in the pattern synonym (see below).

 * But instead of failing, we just added some constraints to solve "later",
 and continued.

 * "Continued" means that we did a `zonkTcTypeToType` (in
 `tc_patsyn_finish`) which defaulted a unification variable to `Any`.

 I'll fix that; essentially we should not attempt to continue if there are
 any unsolved constraints from this pattern synonym.

 The error is a classic GADT one.  Here is a simpler example:
 {{{
 data T a b where
   T1 :: (a~Int) => b -> T a b

 pattern TX <- T1 True
 }}}
 We start with an overall pattern type of `T alpha beta`.  Then, under the
 pattern match of `T1` we need `beta ~ Bool`, and that fails with
 {{{
 T15685.hs:21:17: error:
     * Couldn't match expected type `b' with actual type `Bool'
         `b' is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with constructor:
                      T1 :: forall a b. (a ~ Int) => b -> T a b,
                    in a pattern synonym declaration
           at T15685.hs:21:14-20
       `b' is a rigid type variable bound by
         the inferred type of TX :: T a b
         at T15685.hs:21:9-10
       Possible fix: add a type signature for `TX'
 }}}
 And indeed if we add a signature
 {{{
 pattern TX :: T a Bool
 -- or
 pattern TX :: () => (a~Int) => T a Bool
 }}}
 then all is well.

 The example in the ticket is more complicated, because the untouchable
 variable is a ''kind'' variable.  So the error that is now reported (after
 fixing the `Any` stuff) is
 {{{
 T15685.hs:17:25: error:
     * Kind mismatch: cannot unify (f :: k -> *) with: NP a0 :: [*] -> *
       Their kinds differ.
       Expected type: f a
         Actual type: NP a0 b0
     * In the pattern: Nil
       In the pattern: Here Nil
       In the declaration for pattern synonym `HereNil'
 }}}
 There is actually ''another'', separate kind-level error, which says that
 `k ~ [*]` is insoluble, because `k` is untoucahble.  But currently we
 suppress the kind-level error in favour of the type-level error.

 TL;DR:

 * You need a pattern signature.  That's by-design.

 * But the `Any` business is bogus, and I'll fix that.

 * The same fix also gets rid of the confusing error about `f ~~ NP f0`.
 This was is also the result of "carrying on" too much; it comes from the
 'builder' for `HereNil` which we should not even attempt to typecheck if
 there is an earlier error.

 * The remaining kind error is correct; but not a very good error message.

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