This error (with a very concise name) is given when disambiguation can't decide between distinct copies of a constructor because the expected type of the pattern is underconstrained, meaning we can't compare the types of the copies. The error message doesn't mention this at all - only the name of the expected datatype and of all possible constructors, even the ones that were positively ruled out. For example:
dataBool:Setwheretruefalse:BoolmoduleFoo(b:Bool)wheredataD:Setwherec:DopenmoduleTrue=FootrueopenmoduleFalse=FoofalsedataConfuse:Setwherec:Confusetest:Foo.D?→Settestc=?-- error: [CantResolveOverloadedConstructorsTargetingSameDatatype]-- Can't resolve overloaded constructors targeting the same datatype-- (Test495.Foo.D): Test495.True.c Test495.False.c Test495.Confuse.cThe error is thrown in two places:
- Line 1757 in f561187
(_ , [_]) -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d cs - Lines 1088 to 1090 in f561187
c:cs-> disambiguateByArgs dcs' args $typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $fmap conName $ c :| cs
I think a better error message would be something like:
Can't disambiguate between constructors for type Foo.D ?
Possible candidates:
* Test495.True.c : True.Foo
* Test495.False.c : False.Foo
The new type for the error should then be:
|CantResolveOverloadedConstructorsTargetingSameDatatypeType-- ^ Expected type at position(List1(QName,Type,MaybeTCState))-- ^ Resolved constructor name, its return type, and possibly the new TC state-- The type must be @prettyTCMCtx TopCtx@ /in the new state/ if given, but the-- resulting @Doc@ is freely movable.Note that the QName in the dcs' list in Application.hs is not the name of the constructor. You want conName from the ConHead instead.
This error (with a very concise name) is given when disambiguation can't decide between distinct *copies* of a constructor because the expected type of the pattern is underconstrained, meaning we can't compare the types of the copies. The error message doesn't mention this at all - only the *name* of the expected datatype and of *all possible* constructors, even the ones that were positively ruled out. For example:
```agda
data Bool : Set where
true false : Bool
module Foo (b : Bool) where data D : Set where c : D
open module True = Foo true
open module False = Foo false
data Confuse : Set where c : Confuse
test : Foo.D ? → Set
test c = ?
-- error: [CantResolveOverloadedConstructorsTargetingSameDatatype]
-- Can't resolve overloaded constructors targeting the same datatype
-- (Test495.Foo.D): Test495.True.c Test495.False.c Test495.Confuse.c
```
The error is thrown in two places:
* https://codeberg.org/1lab/mikan/src/commit/f56118785f5e78eca5592a7601a6f547353b8a06/src/full/Mikan/TypeChecking/Rules/LHS.hs#L1757
* https://codeberg.org/1lab/mikan/src/commit/f56118785f5e78eca5592a7601a6f547353b8a06/src/full/Mikan/TypeChecking/Rules/Application.hs#L1088-L1090
I think a better error message would be something like:
```
Can't disambiguate between constructors for type Foo.D ?
Possible candidates:
* Test495.True.c : True.Foo
* Test495.False.c : False.Foo
```
The new type for the error should then be:
```agda
| CantResolveOverloadedConstructorsTargetingSameDatatype
Type
-- ^ Expected type at position
(List1 (QName, Type, Maybe TCState))
-- ^ Resolved constructor name, its return type, and possibly the new TC state
-- The type must be @prettyTCMCtx TopCtx@ /in the new state/ if given, but the
-- resulting @Doc@ is freely movable.
```
Note that the `QName` in the `dcs'` list in `Application.hs` is *not* the name of the constructor. You want `conName` from the `ConHead` instead.