Re: [GHC] #11203: Kind inference with SigTvs is wrong

17 Dec 2015

      #11203: Kind inference with SigTvs is wrong
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
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 goldfire):

 Quite a bit of discussion has led to this general rule:

 * Two user-written type variables, both in scope at the same time, should
 always refer to distinct, unknown types.

 Note that this rule is, in fact, violated sometimes:

 {{{
 f :: a -> a -> Int
 f (x :: b) (y :: c) = 3
 }}}

 This definition is accepted, even though `b` and `c` share a scope and
 refer to the same type. Under the general rule, this should be rejected.
 Now that we have type wildcards, a user who really wanted to write
 something like `f` can use wildcards.

 Returning to the situation in the original ticket, the general rule would
 allow `S`/`T` and prevent `Q`, as desired.

 Now, how to implement: when creating a `SigTv`, we could record the set of
 variables in scope at the time. Then, whenever we unify a `SigTv` with
 another type, we just make sure that the other type can never unify with
 any of those variables.

 Specifically: let's write `SigTv{a,b}` to denote a `SigTv` type variable
 flavor (a `MetaInfo`) that cannot unify with `a` or `b`. A tyvar `b` with
 flavor `SigTv{vs}` may unify with a type `t` only when:

 1. `t` is a type variable, `a`; AND
 2. (`a` is a skolem; OR
 3. `a` is a `SigTv{ws}` such that `ws` is a superset of `vs`)

 Note that `ws` and `vs` may contain other `SigTv`s that have unified; it
 might be necessary to zonk `ws` and `vs` before doing the superset check.

 I offer no justification for why my approach might work. But I think it
 would.

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