Question about implementing `Typeable` (with kinds)

[Adam Gundry]

On 09/02/15 13:20, Simon Peyton Jones wrote:
> I think just add a new constructor to EvTerm.
> 
> Yes, it’s special-purpose, but the **solver* *is special-purpose too. 
>  And it does mean that we know exactly what forms of evidence we can
> generate!

Is there any problem in principle with allowing arbitrary HsExprs inside
an EvTerm? Hopefully that would subsume the type-lits, Typeable and
possible future cases. The grand plan with typechecker plugins is to
make it possible to implement such special-purpose constraint solvers
outside GHC itself; at the moment we can do that for equality
constraints, but not very easily for other sorts of constraints (like
Typeable).

Adam


> 
> *From:*Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
> *Sent:* 07 February 2015 20:11
> *To:* Simon Peyton Jones; ghc-devs at haskell.org
> *Subject:* Question about implementing `Typeable` (with kinds)
> 
>  
> 
> Hello,
> 
>  
> 
> I started adding custom solving for `Typeable` constraints, to work
> around the problem where kind parameters were missing from the
> representation of types. 
> 
>  
> 
> The idea is as follows:
> 
>  
> 
>   1. Add a new filed to `TypeRep` that remembers _kind_ parameters:
> 
>  
> 
>       TypeRep Fingerprint TyCon [TypeRep]{-kinds-} [TypeRep]{-types-}
> 
>  
> 
>   2. Modify the constraint solver, to solve constraints like this:
> 
>      - Kind-polymorphic type constructors don't get `Typeable` instances
> on their own
> 
>      - GHC can solve `Typeable` constraints on  _/concrete uses/_ of
> polymorphic type constructors.
> 
>       More precisely, GHC can solve constraints of the form `Typeable k
> (TC @ ks)`, as long as:
> 
>        (1) `k` is not a forall kind,
> 
>        (2) the `ks` are all concrete kinds (i.e., they have no free kind
> variables).
> 
>  
> 
> This all seems fairly straight-forward, but I got stuck on the actual
> implementation, in particular:
> 
>  
> 
> *what `**EvTerm` should I use when discharging a `**Typeable` constraint?*
> 
>  
> 
> I can create a an `HsSyn` value for the required method (i.e., a
> function of type `Proxy# t -> TypeRep`).
> 
> I can also cast this into a `Typeable` dictionary value.
> 
> The issue is that I am left with an `HsSyn` expression, and not an `EvTerm`.
> 
>  
> 
> So is there a way to treat an arbitrary expression as an `EvTerm`?
> 
>  
> 
> In the implementation of the type-lits, I just added custom evidence,
> but this does not scale well (also, in that case the evidence is just a
> simple value, while here
> 
> it is a bit more complex).
> 
>  
> 
> Suggestions would be most appreciated!
> 
>  
> 
> -Iavor


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/