rigid type variable trouble/suspect Impredicativity

Question

Following on from this q about GADTs, I'm trying to build an EDSL (for the example in the paper) but without GADTs. I have got something working that avoids doubling-up the datatypes for the AST; but instead it seems to be doubling-up the code. So I tried trimming down the code, which is where I've run into trouble ...

Instead of a GADT like so

data Term a where
  Lit ::      Int -> Term Int
  Inc :: Term Int -> Term Int
  IsZ :: Term Int -> Term Bool
  -- etc

declare each constructor as a separate datatype

data Lit   = Lit Int  deriving (Show, Read)
data Inc a = Inc a    deriving (Show, Read)
data IsZ a = IsZ a    deriving (Show, Read)
-- etc

Then the EDSL user can enter and show terms

aTerm = IsZ (Inc (Lit 5))

illtypedTerm = Inc (IsZ (Lit 5))    -- accepted OK and can show
                                    -- but can't eval [good!]

Then to catch that they're all Terms and need to be well-typed

data Term a = ToTerm { fromTerm :: a} deriving (Show, Eq)

class IsTerm a c  | a -> c 
instance IsTerm Lit (Term Int) 
-- etc

The FunDep captures the return type from the original GADT. Then eval can use that Term type

class Eval a   
  where eval :: (IsTerm a c) => a -> c 
                             -- hmm this makes 'c' a rigid tyvar
instance Eval Lit  where    
         eval (Lit i) = -- undefined     -- accepted OK, infers :: Term Int
                        ToTerm i         -- rejected

The equation eval (Lit i) = undefined (commented out) compiles OK, and GHC infers eval (Lit 5) :: Term Int. But if I put = ToTerm i:

* Couldn't match expected type `c' with actual type `Term Int'
  `c' is a rigid type variable bound by
    the type signature for:
      eval :: forall c. IsTerm Lit c => Lit -> c
* Relevant bindings include
    eval :: Lit -> c

If GHC can infer (via the FunDep) that c must be Term Int for = undefined, why can't it for = ToTerm i? Is the specialised type sig it's inferred eval :: forall c. IsTerm Lit c => Lit -> c Impredicative? But c is the return type, so it's not RankN(?)

What avoids this error? I do have working

• class (IsTerm a c) => Eval a c | a -> c where ... this just duplicates all the instance heads from IsTerm, so the superclass constraint is only acting as belt and braces. (That's the doubling-up I was trying to avoid.)

• type family ToTerm a ...; class Eval a where eval :: a -> ToTerm a. But again the instances for Eval double-up all the instances for ToTerm, and furthermore need large contexts with many ~ constraints between ToTerm calls.

I could just throw away class IsTerm, and put all the Term-inference on class Eval. But I was trying to closely mirror the GADT style such that I might have many application 'clients' sharing the same definition for Term.

Addit: [March 14]

The 2011 paper System F with Type Equality Coercions, Section 2.3, has this example (in discussing Functional Dependencies)

class F a b | a -> b
instance F Int Bool

class D a where { op :: F a b => a -> b }
instance D Int where { op _ = True }

Using FC, this problem [of typing the definition of op in the instance D Int] is easily solved: the coercion in the dictionary for F enables the result of op to be cast to type b as required.

• This example seems to be the same as the q, with class F, with FunDep, being IsTerm and class D being Eval.

• This example doesn't compile: gives the same rejection as IsTerm/Eval.

Ermey

https://mcmap.net/q/1917642/-printing-church-booleans q & answer seems to apply: the instance here returning ToTerm i is not allowing just any type for c. OTOH it is allowing any type that meets the IsTerm a c => constraint on method eval. So(?) GHC is ignoring the constraint? Or isn't clever enough to see the constraint has a FunDep that improves c to exactly the type of ToTerm i. – Ermey

Answer 1

If GHC can infer (via the FunDep) that c must be Term Int for = undefined

It can't. If you try undefined :: Term Int, you'll get the same rigid type variable error. If you use a typed hole = _undefined you'll see it's inferring undefined :: c. I don't know why, but the functional dependency only seems to be used when applying eval to Lit, not when defining it.

What about this?

class IsTerm a where
  type TermType a :: *
instance IsTerm Lit where
  type TermType Lit = Int
instance IsTerm a => IsTerm (Inc a) where
  type TermType (Inc a) = TermType a

class IsTerm a => Eval a   
  where eval :: a -> Term (TermType a) 

instance Eval Lit  where    
         eval (Lit i) = ToTerm i

-- needs UndecidableInstances
instance (Eval a, Num (TermType a)) => Eval (Inc a)  where    
         eval (Inc i) = ToTerm (fromTerm (eval i) + 1)

Ignatzia

"It can't ... I don't know why". Other qs on rigid type variables suggest I need a RHS of type no less general than bare c. So is the IsTerm constraint just ignored? Your suggestion of associated TF TermType seems even more verbose than my top-level TF ToTerm; why make it associated? What I mean by "large contexts" is for data If b a1 a2 = ... whose Eval instance requires IsTerm b (Term Bool) and the Term type of a1, a2 to be the same, and that's the type of the result. The instance for a two-param Eval is more succinct, even with the repetition. – Ermey

Answer 2

Note that the IsTerm constraint is on method eval, not a superclass constraint on Eval -- it couldn't be there because the return type c of eval is not a parameter to the class.

Then it's misleading to consider instance Eval Lit in isolation. Consider the instance for Inc, and its instance for IsTerm:

instance ( {-# tba #-} ) => Eval (Inc a)  where
  eval (Inc i) = ToTerm $ 1 + fromTerm (eval i)

instance (IsTerm a (Term int)) => IsTerm (Inc a) (Term Int)

What should that tba constraint include?

• The method body has a recursive call to eval, so it needs Eval a for that.
• The method body's 1 + ... eval ... needs eval to return an Int, but the Eval constraint doesn't provide that (because it doesn't mention the return type).
• Could a constraint IsTerm a (Term Int) provide it? No: IsTerm is (at best) implied by Eval, not the other way round.

So the only way this could hang together without a lot of duplication is if:

• The compiler saw the recursive call to eval; magically added an IsTerm a c1 constraint for it; found the applicable instance of IsTerm for a; and then figured out that IsTerm instance yielded c1 ~ Term Int.
• But if all it has is bare a, there's no way to know which instance. So leave the constraint as Wanted pending getting eval applied to (Inc x) for some term x?

Contrast that in the GADT definition for Inc, its argument needs to be Term Int. This is the straitjacket that prevents an EDSL user entering an ill-typed term:

  Inc :: Term Int -> Term Int

As to the specific rejection message for the instance Eval Lit, I think Hugs' wording makes it clearer:

- Inferred type is not general enough
*** Expression    : eval
*** Expected type : (Eval Lit, IsTerm Lit a) => Lit -> a
*** Inferred type : (Eval Lit, IsTerm Lit (Term Int)) => Lit -> Term Int

The 'Expected type' is the method's signature with the instance head substituted in. To typecheck a method body whose type is not 'general enough' would need:

1. seeing the method's constraint as part of checking the method's body;
2. seeing that the class for that constraint has a FunDep, and that it improves the return type from the argument type;
3. finding the applicable instance of IsTerm for the instance of Eval (and instances for any constraints on that instance, recursively);
4. improving c to Term int via the FunDep.

Step 3. in particular is too much to expect: the applicable instance(s) might be declared in a separate module, which is not in scope; in general (unlike this example) it might need an instance for a type scheme/the available instances might be more specific or more general/can't be picked until types are more refined.

But I do have an outstanding question:

• If the type of the method's body is more specific than inferred by substituting in the instance head, what goes wrong?
• The inferred type in the Hugs message is more specific, but also carries the constraints, so they must be discharged for the program to be accepted.
• If the caller of eval is expecting a more general type, the more specific result can substitute in.

Ermey

Answer 3

I'm posting another answer because it's quite a surprise/a rare beast: code that compiles under Hugs and works; but doesn't compile under GHC (8.6.4). That is unless someone here can see I've gone wrong and can fix it up.

Consider first the Addit: example from the 2011 paper. This achieves it in Hugs only (WinHugs 'latest' release Sep 2006)

class F a b | a -> b
instance F Int Bool

class D a where { op :: (F a b) => a -> b } 
instance (TypeCast Bool b') => D Int where { op _ = typeCast True }

That code is same as in the paper except for the instance D Int. I've added a TypeCast constraint (and call to its method), which looks weird because type variable b' isn't used anywhere.

I've tried various ways round to get that to compile in GHC:

• The TypeCast is approximately equal to GHC's ~ constraint, which is not a feature in Hugs; but changing it to ~ won't get GHC to accept the code.
• I've tried various type annotations, including with ScopedTypeVariables. Nada.

See Trac #16430 for more details, including the definition for TypeCast -- which is entirely standard.

Then the code for the original q here goes like this (Hugs only)

class    Eval a   where
         eval :: (IsTerm a c) => a -> c 

instance (TypeCast (Term Int) c') => Eval Lit  where
         eval (Lit i) = typeCast (ToTerm i)       -- rejected without typeCast

instance (Eval a, IsTerm a (Term Int), TypeCast (Term Int) c')
         => Eval (Inc a)  where
         eval (Inc i) = typeCast (ToTerm $ 1 + fromTerm (eval i))
instance (Eval a, IsTerm a (Term Int), TypeCast (Term Bool) c') 
         => Eval (IsZ a)  where
         eval (IsZ i) = typeCast (ToTerm $ 0 == fromTerm (eval i))

eval aTerm (see the q above) now returns (ToTerm False); eval illtypedTerm gives a rejection message, as expected.

All of those instances feature that TypeCast to a dangling type variable (if "feature" is the right word). It's debatable whether I've achieved any saving of duplicated code as against making Eval a class with two parameters that just repeats from IsTerm.

Ermey