search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Kind polymorphism introduces spurious variables #107

Closed antalsz closed 6 years ago

antalsz commented 6 years ago

In Data.Semigroup.Internal, we have

newtype Alt f a = Alt {getAlt :: f a}

Which is secretly

newtype Alt {k} (f :: k -> Type) (a :: k) = Alt {getAlt :: f a}

Even when we specify the kind annotation using a data kinds edit, we still introduce spurious kind variables sometimes, such as in

Program Instance Eq___Alt {k} {f} {a} `{GHC.Base.Eq_ (f a)}
   : GHC.Base.Eq_ (Alt f a : GHC.Prim.TYPE GHC.Types.LiftedRep) :=
  fun _ k =>
    k {| GHC.Base.op_zeze____ := Eq___Alt_op_zeze__ ;
         GHC.Base.op_zsze____ := Eq___Alt_op_zsze__ |}.

This then fails to typecheck because it can't deduce anything about {k}.