Skip to content

Namespace collision detection for promoted types

In the following example

{-# LANGUAGE DataKinds #-}

module Foo where

data Nat = Z | S Nat

data S

foo :: S n -> S n
foo = id

GHC displays the error

Foo.hs:12:8:
    ‘S’ is applied to too many type arguments
    In the type signature for ‘foo’: foo :: S n -> S n
Failed, modules loaded: none.

Of course this code compiles without the definition of data S. Without namespace collision detection, it is easy to have working code, and then import a module which breaks the code. For example, I made this request after I imported Module1 with type S defined and Module2 with the promoted type S, which is what I was trying to use.

Can we get namespace collision detection instead? I'm proposing something like:

Foo.hs:9:15
    Ambiguous occurence ‘S’
    It could refer to either Foo.S defined at Foo.hs:7:1
                          or to Foo.'S promoted from the constructor defined at Foo.hs:5:16
                          or to `Bar.'S` promoted from the constructor defined at Bar.hs:line#:char# 
                          or to ...
    Use 'S to refer to promoted constructors.
Edited by Eric Crockett
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information