## Investigate touchable meta-variables in Givens

@simonpj believes it would be disastrous to ever have a touchable meta-variable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:

```
{-# LANGUAGE PolyKinds, PartialTypeSignatures #-}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a -> ()
f :: C a => Proxy a -> _
f p = meth p
```

The partial signature for `f`

is not kind-generalized (the fact that it is partial means that we might want the definition of `f`

to inform the kind of `a`

) and thus the kind of `a`

remains as a meta-variable `kappa`

. In the body of `f`

, we have `[G] C kappa a`

. We can see this in this snippet of `-ddump-tc-trace`

(with `-fprint-explicit-kinds`

enabled):

```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```

The variable `k_aoT[tau:1]`

is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)

This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.