Changes between Version 5 and Version 6 of GhcKinds/KindInference/Examples


Ignore:
Timestamp:
Oct 26, 2018 1:50:05 PM (10 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindInference/Examples

    v5 v6  
    129129This should be accepted with `T3 :: forall k. k -> k -> Type`; it's not polymorphically recursive. Yet, it would seem any specification which accepted `T` would also give `T3` the polymorphically recursive kind `forall k1 k2. k1 -> k2 -> Type`.
    130130
     131{{{#!hs
     132data T4 k (a :: k) b = MkT4 (T4 k b a)
     133}}}
     134
     135Here, we have a dependent kind for `T4`. Richard thinks this should be accepted. Proposed rule: dependent variables must be fixed an unchanging at all occurrences within a mutually recursive group (otherwise, we have polymorphic recursion). That is, it would be an error to mention, say, `T4 k2` anywhere in the body of `T4`: it must be `T4 k`.
     136
     137== Generalization
     138
     139Contrast
     140
     141{{{#!hs
     142class C8 a where
     143  meth :: Proxy (a :: k)
     144}}}
     145
     146with
     147
     148{{{#!hs
     149data V1 a where
     150  MkV1 :: Proxy (a :: k) -> V1 a
     151}}}
     152
     153Currently (GHC 8.6) we reject `C8` while accepting `V1`. This may be just a bug, but it has to do with the fact that the type of `meth` isn't quantified over `a`, but it is over `k` (lexically).
     154
    131155== Dependency ordering
    132156