Re: [GHC] #9607: Type checking regression between GHC 7.6 and 7.8

18 Sep 2014

      #9607: Type checking regression between GHC 7.6 and 7.8
-------------------------------------+-------------------------------------
              Reporter:  jstolarek   |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Indeed, and there is a good reason for that: when you call `rightUnit`,
 its unclear how to instantiate `n`; its type is indeed ambiguous.  For
 example, if you write this
 {{{
 rightUnit1 :: Tensor s -> Tensor (s ++ '[n, n])
 ru1 = rightUnit
 }}}
 you might expect it to be accepted.  After all, that ''is'' the type of
 `rightUnit`!  But it's rejected thus:
 {{{
 T9607.hs:34:7:
     Couldn't match type ‘s ++ '[n0, n0]’ with ‘s ++ '[n, n]’
     NB: ‘++’ is a type function, and may not be injective
     The type variable ‘n0’ is ambiguous
     Expected type: Tensor s -> Tensor (s ++ '[n, n])
       Actual type: Tensor s -> Tensor (s ++ '[n0, n0])
     Relevant bindings include
       ru1 :: Tensor s -> Tensor (s ++ '[n, n]) (bound at T9607.hs:34:1)
     In the expression: rightUnit
     In an equation for ‘ru1’: ru1 = rightUnit
 }}}
 This perplexing behaviour is ruled out by the default of
 `-XNoAllowAmbiguousTypes`.

 However your example is useful because it shows an example where a
 function with an ambiguous type can nevertheless be called in an entirely
 unambiguous way.  The call in `userightUnit` instantiates the type of
 `rightUnit` with (say) `s = ss` and `n = nn`.  Now we get the following
 constraints:
 {{{
   Tensor ss ~ Tensor [1]                     -- From the argument of
 rightUnit
   Tensor (ss ++ [nn, nn]) ~ Tensor [1,2,2]   -- From the result of
 rightUnit
 }}}
 solving the first gives `ss ~ [1]`.  Substituting in the second gives
 {{{
   [1] ++ [nn,nn] ~ [1,2,2]
 }}}
 Now use the equations for `++` and you can see this is readily solved by
 `nn ~ 2`.

 In short, ''some'' calls to `rightUnit` will give rise to ambiguity, but
 not all.

 It's not clear what "better" behaviour might be. One thing I can think of
 is this:
  * Allow ambiguous user-written type signatures
  * But do not infer ambiguous types
 I.e. if you want a function to get an ambiguous type you must say so.

 See also #9587

 Simon

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