GADT and proof of equality

Question

I want to hide some type information in a GADT, here forgetting about the key type

data Query  where
   Query :: Ord key =>  Map.Map key String  -> Query

 one ::  Ord key => key -> Query
 one  k =
   let m = Map.insert k "hello" Map.empty
   in Query m

How can I pass on some equality constraint to use it elsewhere as in :

other :: Ord key => key -> Query -> Maybe String
other k (Query ad) =  Map.lookup k ad

Answer 1

– leftaroundabout Jan 6 at 17:19

If you just keep the type variable visible – but universally-quantified – then everybody else has to treat it abstractly too, but it's still there for when you want to access it and apply whatever constraints you have floating around. — If you actually have a global proof that all keys have the same type, then you should not make it a variable at all. If you have only two or three such types (and don't plan to allow many more), you shouldn't use a type variable either, but a variant type which has discrete options for the different instantiations.