CODEWITHSUNDEEP
haskelltypes
Siddharth Bhat
Siddharth Bhat

Reputation: 843

Rank 2 constraint programming / constraint implication

import Data.Constraint

reify :: (c' :- c) -> (c => a) -> (c' => a)
reify cons f = case cons of Sub d -> case d of Dict -> f

Using reify, I can weaken a constraint c to a constraint c' given proof that c' implies c.

Now, I want a Rank2 variant of this:

-- reify2 Rank2's reify
reify2 :: (forall r1. c' r1 :- c r1) -> 
          (forall r2. c r2 => a) -> 
          (forall r3. c' r3 => a)
reify2 cons f = ???

But I'm unable to implement such a function, even though it must "clearly" be possible.

Upvotes: 1

Views: 103

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33399

The ambiguity can be lifted using ScopedTypeVariables+TypeApplications, although you need to reorder the arguments of reify2, putting the type arguments first to put them in scope.

{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, ConstraintKinds, GADTs, ScopedTypeVariables, TypeApplications, TypeOperators #-}

data Dict c where
  Dict :: c => Dict c

data c :- d where
  Sub :: (c => Dict d) -> c :- d

reify2 :: forall r3 c c' a. c' r3 =>
          (forall r1. c' r1 :- c r1) ->
          (forall r2. c r2 => a) ->
          a
reify2 cons f =
  case cons @r3 of
    Sub Dict -> f @r3

Upvotes: 2

Related Questions