[GHC] #14449: Type variables allowed to unify in a partial type signature (PartialTypeSignatures)

10 Nov 2017

      #14449: Type variables allowed to unify in a partial type signature
(PartialTypeSignatures)
-------------------------------------+-------------------------------------
           Reporter:  kcsongor       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 During a discussion today, Richard discovered the following bug:

 The function `f` is accepted in GHC 8.2.1 (and HEAD too):

 {{{#!hs
 {-# LANGUAGE PartialTypeSignatures #-}

 f :: a -> b -> _
 f x y = [x, y]
 }}}

 with the warning:

 {{{
 Bug.hs:3:16: warning: [-Wpartial-type-signatures]
     • Found type wildcard ‘_’ standing for ‘[a]’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of f :: a -> a -> [a] at Bug.hs:4:1-13
     • In the type signature: f :: a -> b -> _
   |
 3 | f :: a -> b -> _
   |                ^
 Ok, 1 module loaded.

 }}}

 This is a regression compared to 8.0.1, where the following error is
 produced (rightly):

 {{{
 Bug.hs:4:12: error:
     • Couldn't match expected type ‘a’ with actual type ‘b’
       ‘b’ is a rigid type variable bound by
         the inferred type of f :: a -> b -> [a]
         at Bug.hs:3:6
       ‘a’ is a rigid type variable bound by
         the inferred type of f :: a -> b -> [a]
         at Bug.hs:3:6
     • In the expression: y
       In the expression: [x, y]
       In an equation for ‘f’: f x y = [x, y]
     • Relevant bindings include
         y :: b (bound at Bug.hs:4:5)
         x :: a (bound at Bug.hs:4:3)
         f :: a -> b -> [a]
           (bound at Bug.hs:4:1)
 Failed, modules loaded: none.

 }}}

 Note that the inferred type of `f` is still correct: `f :: a -> a -> a`,
 but the type variables `a` and `b` are allowed to unify during inference,
 and they shouldn't be. If I understood correctly, this implies that when
 inferring the type of functions with partial type signatures, the type
 variables are (wrongly) treated as `SigTv`s, instead of skolem constants.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14449
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler