Type parameter in context which cause some ambiguity

Question

I have the following error for the cadr1 below, which makes sense

Could not deduce (BoolEq n ('Succ ('Succ n'0)) ~ 'True)

from the context (BoolEq n ('Succ ('Succ n')) ~ 'True)

The type variable ‘n'0’ is ambiguous

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE TypeFamilies   #-}

module DecidablePropositionalEquality where


data Nat = Zero | Succ Nat

data Vec :: * -> Nat -> * where
  VNil  :: Vec a Zero
  VCons :: a -> Vec a n -> Vec a (Succ n)

type family Greater (a:: Nat) (b:: Nat) :: Bool where
  Greater Zero Zero = True
  Greater Zero (Succ x) = False
  Greater (Succ x) Zero = True
  Greater (Succ a) (Succ b) = Greater a b

op :: forall a n n'. (Greater n (Succ (Succ n')) ~ True) => Vec a n -> a 
op v = undefined

I don't use n' at the definition site, so it is ambiguous.

Is there anyway for me to existentially quantify over this n', so that ghc does not try to assign it to some type, and fails as nothing ties it to anything ?

More generally, how to control the scope of those type variables ?

edit : modified to remove Boolean type family

Why not `cadr1 :: forall a n'. Vec a (Succ (Succ n')) -> a` ? — chi, Jun 30 '17 at 16:50
Sounds like an excellent solution for that specific case. but I wonder if there are ways to remove/scope (via quantification) those names. Here I would like `n'` to be scoped to this code. and since I intend to not use anything from it, its mere existence is fine. and it should not be 'ambiguous' it GHC does not try to assign it to something out of its intended scope — nicolas, Jun 30 '17 at 17:19
Boolean type families are the #1 [most](https://stackoverflow.com/q/37923470/1523776) [common](https://stackoverflow.com/q/38209817/1523776) [antipattern](https://stackoverflow.com/q/38290067/1523776) I see in Stack Overflow questions about dependently typed Haskell. `n ~ Succ (Succ n')` is a perfectly good constraint and is not ambiguous. — Benjamin Hodgson, Jun 30 '17 at 18:28
@BenjaminHodgson :)) ok it's a outbreak. you seem to have a valid point for the BoolEq case, I was trying to come up with something simple where we **do** have a ambiguity, not trying to find ways to avoid it. — nicolas, Jun 30 '17 at 18:54
@nicolas I see. The general remedy for this is "use a better design", though that's not particularly useful advice, haha. The better design in question depends on the situation, of course. We'd probably be able to give you more advice if the code in your question was more representative of the real-life code in which you're seeing this problem? — Benjamin Hodgson, Jun 30 '17 at 19:03
@BenjaminHodgson Thank you. I was more curious as to how such names are dealt with currently in haskell as of now. notably how to control their scope. but I guess that your answer of "use a better design" is saying nonetheless, like the AllowAmbiguousTypes pragma, or resorting to Singletons (afaik) — nicolas, Jun 30 '17 at 19:41
Even if you enable `AllowAmbiguousTypes`, the `n'` type parameter is entirely useless - types are erased at runtime, so there is absolutely no way to compute with it inside the body of `op`. You need a type class constraint on `n'`, or a singleton storing its value, or something of the sort. You are probably thinking of something like the user calling e.g. `op @5` and getting a parametric function which always produces a vector of a least length `7`; but with the given type, you simply could not implement such a function. — user2407038, Jun 30 '17 at 21:50

Type parameter in context which cause some ambiguity

0 Answers0