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.

stackoverflow.com/questions/55077731/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. — AntC

Alexey Romanov Alexey Romanov · Accepted Answer · 2019-03-07T16:39:58

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)

rigid type variable trouble/suspect Impredicativity

3 Answers