ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Constructing coercion for associated type instance #106

Open conal opened 10 years ago

conal commented 10 years ago

Are there any mechanisms for constructing coercions for associated type instances? For instance, I have a class:

class Encodable a where
  type Encode a
  encode :: a -> Encode a
  decode :: Encode a -> a

and an instance

instance (Encodable a, Encodable b) => Encodable (a -> b) where
  type Encode (a -> b) = Encode a -> Encode b
  encode = decode --> encode
  decode = encode --> decode

where

infixr 1 -->
-- | Add pre- and post processing
(-->) :: (a' -> a) -> (b -> b') -> ((a -> b) -> (a' -> b'))
(f --> h) g = h . g . f

Now I want to find/construct a coercion from Encode (Bool -> Bool) to Encode Bool -> Encode Bool that I can then use in a Cast.

conal commented 10 years ago

I also need to find what the associated type is for a given type function and argument. I'll ask on the ghc-devs list.

conal commented 10 years ago

Heard from Richard Eisenberg about "Constructing coercions for associated type":

Richard Eisenberg said

Does FamInstEnv.normaliseType work for you? FamInstEnv is in the types/ directory. FamInst.tcGetFamInstEnvs may also be helpful. FamInst is in the typecheck/ directory.

Looks like just the thing. I may give it a try myself when the issue pops up again if no one beats me to it.

xich commented 10 years ago

To construct the FamInstEnvs argument you need, you can do:

normaliseTypeT :: (HasModGuts m, HasHscEnv m) => Role -> Transform c m Type (Coercion, Type)
normaliseTypeT r = do
  envs <- constT $ do
    guts <- getModGuts
    eps <- getHscEnv >>= liftIO . hscEPS 
    return (eps_fam_inst_env eps, mg_fam_inst_env guts) 
  arr (normaliseType envs r)
conal commented 10 years ago

Thanks! I think I'll give it a try.