agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Allow `existing-class` for postulated type classes

Open flupe opened this issue 1 year ago • 0 comments

We should enable the existing-class pragma for postulated type classes:

postulate
  MyShow : Set -> Set
  myshow : {{ MyShow a }} -> a -> String
{-# COMPILE MyShow existing-class #-}

ok : {{ MyShow a }} -> a -> String
ok = myshow

Currently MyShow is not considered a class (since #284), and thus the instance arguments get turned into regular Haskell arguments and not class constraints:

ok : MyShow a -> a -> String
ok x = myshow x

flupe avatar Oct 01 '24 12:10 flupe